theorem
proved
tactic proof
countLaw_implies_card
show as:
view Lean formalization →
formal statement (Lean)
89theorem countLaw_implies_card {D : ℕ} {Family : Type} [Fintype Family]
90 {encoding : Family → F2Power D} (hL : CountLaw D Family encoding) :
91 Fintype.card Family = 2 ^ D - 1 := by
proof body
Tactic-mode proof.
92 have himage : Finset.univ.image encoding =
93 Finset.univ.filter (fun v : F2Power D => v ≠ 0) := by
94 apply Finset.Subset.antisymm
95 · intro v hv
96 rcases Finset.mem_image.mp hv with ⟨x, _, hx⟩
97 rw [Finset.mem_filter, ← hx]
98 exact ⟨Finset.mem_univ _, hL.nonzero x⟩
99 · intro v hv
100 rw [Finset.mem_filter] at hv
101 rcases hL.surjective_on_nonzero v hv.2 with ⟨x, hx⟩
102 exact Finset.mem_image.mpr ⟨x, Finset.mem_univ _, hx⟩
103 have hcard : (Finset.univ.image encoding).card = Fintype.card Family := by
104 rw [Finset.card_image_of_injective _ hL.injective]
105 rfl
106 rw [← hcard, himage, F2Power.nonzero_card]
107
108/-! ## §3. The universal "no extra family member" theorem -/
109
110/-- Universal "no eighth member" theorem: every non-zero vector is
111 the encoding of some family member. (Just a re-statement of the
112 surjectivity field, for symmetric naming.) -/