English
An induction principle for closure membership with symmetric differences and suprema: if p is preserved under sdiff and sup and complement, then p holds throughout closure s.
Русский
Индуктивный принцип для замыкания с симметрическими разностями и объединениями: если p сохраняется при sdiff и sup и дополнениях, то она держится на всем closure s.
LaTeX
$$closure_sdiff_sup_induction IsSublattice s → bot_mem → top_mem → ∀ {p : (g : α) → SetLike.instMembership.mem (BooleanSubalgebra.closure s) g → Prop}, (∀ (x : α) (hx : Set.instMembership.mem s x) (y : α) (hy : SetLike.instMembership.mem (BooleanSubalgebra.closure s) y), p (inst.sdiff x y) ⋯) → (∀ (x : α) (hx : SetLike.instMembership.mem (BooleanSubalgebra.closure s) x) (y : α) (hy : SetLike.instMembership.mem (BooleanSubalgebra.closure s) y), p x hx → p y hy → p (SemilatticeSup.toMax.max x y) ⋯) → ∀ (x : α) (hx : SetLike.instMembership.mem (BooleanSubalgebra.closure s) x), p x hx$$
Lean4
@[elab_as_elim]
theorem closure_sdiff_sup_induction {p : ∀ g ∈ closure s, Prop}
(sdiff : ∀ x hx y hy, p (x \ y) (sdiff_mem (subset_closure hx) (subset_closure hy)))
(sup : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (sup_mem hx hy)) (x) (hx : x ∈ closure s) : p x hx :=
by
obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mp hx
revert hx
classical
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
simp only [Finset.sup_insert] at hxt ⊢
exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩) (sdiff _ x.1.2 _ x.2.2) (ih _)
