75structure CountLaw (D : ℕ) (Family : Type) [Fintype Family] 76 (encoding : Family → F2Power D) : Prop where 77 /-- The encoding is injective on `Family`. -/ 78 injective : Function.Injective encoding 79 /-- The encoding image avoids the zero vector. -/ 80 nonzero : ∀ x : Family, encoding x ≠ 0 81 /-- Every non-zero vector is in the image of `encoding`. -/ 82 surjective_on_nonzero : 83 ∀ v : F2Power D, v ≠ 0 → ∃ x : Family, encoding x = v 84 85/-! ## §2. The universal cardinality theorem -/ 86 87/-- If `CountLaw` holds for some encoding, then the family has 88 cardinality exactly `2 ^ D - 1`. -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.