English
Under the same hypotheses as mem_closure_iff_sup_sdiff, a membership equivalence holds with a structured finite representation.
Русский
При тех же предположениях, что и mem_closure_iff_sup_sdiff, верна эквивалентность принадлежности с конечной репрезентацией.
LaTeX
$$IsSublattice(s) → bot_mem → top_mem → ∀ a, Iff (a ∈ closure(s)) (Exists t : Finset (Prod s.Elem s.Elem), a = t.sup (fun x => inst.sdiff x.fst.val x.snd.val))$$
Lean4
/-- An induction principle for closure membership. If `p` holds for `⊥` and all elements of `s`, and
is preserved under suprema and complement, then `p` holds for all elements of the closure of `s`. -/
@[elab_as_elim]
theorem closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx, p x (subset_closure hx))
(bot : p ⊥ bot_mem) (sup : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (supClosed _ hx hy))
(compl : ∀ x hx, p x hx → p xᶜ (compl_mem hx)) {x} (hx : x ∈ closure s) : p x hx :=
have inf ⦃x hx y hy⦄ (hx' : p x hx) (hy' : p y hy) : p (x ⊓ y) (infClosed _ hx hy) := by
simpa using compl _ _ <| sup _ _ _ _ (compl _ _ hx') (compl _ _ hy')
let L : BooleanSubalgebra α :=
{ carrier := {x | ∃ hx, p x hx}
supClosed' := fun _a ⟨_, ha⟩ _b ⟨_, hb⟩ ↦ ⟨_, sup _ _ _ _ ha hb⟩
infClosed' := fun _a ⟨_, ha⟩ _b ⟨_, hb⟩ ↦ ⟨_, inf ha hb⟩
bot_mem' := ⟨_, bot⟩
compl_mem' := fun ⟨_, hb⟩ ↦ ⟨_, compl _ _ hb⟩ }
closure_le (L := L).mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
