English
An induction principle for membership in closure: if a property p holds for ⊥ and all elements of s, is preserved under suprema and complement, then p holds for all elements of closure s.
Русский
Индуктивный принцип для принадлежности замыканию: если свойство p выполняется для ⊥ и всех элементов s, сохраняется под объединением и дополняющим, то оно выполняется для всех элементов closure(s).
LaTeX
$$@[elab_as_elim] \\text{closure_bot_sup_induction }$$
Lean4
theorem mem_closure_iff_sup_sdiff {a : α} : a ∈ closure s ↔ ∃ t : Finset (s × s), a = t.sup fun x ↦ x.1.1 \ x.2.1 := by
classical
refine ⟨closure_bot_sup_induction (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
· rintro ⟨t, rfl⟩
exact
t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _ fun x hx ↦
sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2)
· rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩
exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩
rintro x - ⟨t, rfl⟩
refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_
simp_rw [Finset.sup_insert, compl_sup, eq]
refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_
simp_rw [Finset.sup_insert, inf_sup_left, eq]
use {(z, ⟨_, isSublattice.supClosed x.2 w.2⟩), (⟨_, isSublattice.infClosed y.2 z.2⟩, w)} ∪ t
simp_rw [Finset.sup_union, Finset.sup_insert, Finset.sup_singleton, sdiff_eq, compl_sup, inf_left_comm z.1, compl_inf,
compl_compl, inf_sup_right, inf_assoc]
