Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.dense_induction

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {p : M → Prop} (x : M) {s : Set M},
  (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

If s is a dense set in a structure M, Substructure.closure L s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p is preserved under function symbols.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.Structure