Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.closure_induction

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {p : M → Prop} {x : M},
  x ∈ (FirstOrder.Language.Substructure.closure L).toFun s →
    (∀ x ∈ s, p x) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (Set.ofPred p)) → p x

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.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

3 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.Structure