Theorems · Definition · logic and foundations
FirstOrder.Language.empty
FirstOrder.Language
The empty language has no symbols.
- Defined in
- Mathlib.ModelTheory.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement · cited by 1,084
Cited by10
Results whose statement or proof uses this declaration.
- FirstOrder.Language.empty.isFraisseLimit_of_countable_infinitestatement and proof · cited by 1
- FirstOrder.Language.empty.nonempty_equiv_iffstatement and proof · cited by 1
- FirstOrder.Language.emptyStructurestatement and proof · cited by 1
- FirstOrder.Language.card_emptystatement and proof · cited by 1
- Cardinal.empty_theory_categoricalstatement and proof · cited by 1
- Function.emptyHomstatement and proof · cited by 1
- FirstOrder.Language.empty.isFraisse_finitestatement and proof · cited by 0
- FirstOrder.Language.empty.nonempty_embedding_iffstatement and proof · cited by 0
- Cardinal.empty_infinite_Theory_isCompletestatement and proof · cited by 0
- Function.emptyHom_toFunstatement and proof · cited by 0