closure_induction — Mathlib

English

If S_i is a directed family of substructures, then x belongs to the supremum ⨆ i, S_i iff there exists i with x ∈ S_i.

Русский

Пусть S_i образуют направленную семейство подструктур; тогда x принадлежит их супремуму тогда и только тогда, когда существует i с x ∈ S_i.

LaTeX

$$$$ x \in \bigvee_i S_i \iff \exists i, x \in S_i. $$$$

Lean4

/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under function symbols, then `p` holds for all elements of the closure of `s`. -/
@[elab_as_elim]
theorem closure_induction {p : M → Prop} {x} (h : x ∈ closure L s) (Hs : ∀ x ∈ s, p x)
    (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)) : p x :=
  (@closure_le L M _ ⟨setOf p, fun {_} => Hfun⟩ _).2 Hs h

Похожие утверждения