Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le

∀ {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [Nonempty M] [inst : L.Structure M]
  [M ⊨ T],
  Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} (Cardinal.mk M) →
    ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Defined in

Mathlib.ModelTheory.Satisfiability

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonemptyFirstOrder.Language.StructureFirstOrder.Language.Theory.Model