Theorems · Definition · logic and foundations
FirstOrder.Language.IsRelational
FirstOrder.Language → Prop
A language is relational when it has no function symbols.
- Defined in
- Mathlib.ModelTheory.Basic
- Cited by
- 10 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement and proof · cited by 1,084
- IsEmptyproof · cited by 759
- FirstOrder.Language.Functionsproof · cited by 153
Cited by11
Results whose statement or proof uses this declaration.
- FirstOrder.Language.LHom.ofIsEmptystatement and proof · cited by 6
- FirstOrder.Language.Structure.FG.finitestatement and proof · cited by 3
- FirstOrder.Language.Substructure.FG.finitestatement and proof · cited by 3
- FirstOrder.Language.Substructure.closure_eq_of_isRelationalstatement and proof · cited by 2
- FirstOrder.Language.Substructure.mem_closed_of_isRelationalstatement and proof · cited by 2
- FirstOrder.Language.LHom.ofIsEmpty_onFunctionstatement and proof · cited by 0
- FirstOrder.Language.LHom.ofIsEmpty_onRelationstatement and proof · cited by 0
- FirstOrder.Language.Substructure.fg_iff_finitestatement and proof · cited by 0
- FirstOrder.Language.LHom.ofIsEmpty.congr_simpstatement and proof · cited by 0
- FirstOrder.Language.Structure.fg_iff_finitestatement and proof · cited by 0
- FirstOrder.Language.Substructure.mem_closure_iff_of_isRelationalstatement and proof · cited by 0