Theorems · Theorem · logic and foundations
FirstOrder.Language.model_nonemptyTheory_iff
∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], M ⊨ L.nonemptyTheory ↔ Nonempty M- Defined in
- Mathlib.ModelTheory.Semantics
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.cast_oneproof · cited by 2,501
- FirstOrder.Languagestatement and proof · cited by 1,084
- Cardinal.mkproof · cited by 942
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Sentenceproof · cited by 127
- FirstOrder.Language.Theory.Modelstatement · cited by 67
- FirstOrder.Language.Sentence.Realizeproof · cited by 62
- FirstOrder.Language.Sentence.cardGeproof · cited by 3
- FirstOrder.Language.nonemptyTheorystatement · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- FirstOrder.Language.ElementarilyEquivalent.nonempty_iffproof · cited by 1