Theorems · Definition · logic and foundations
FirstOrder.Language.Term.equal
{L : FirstOrder.Language} → {α : Type u'} → L.Term α → L.Term α → L.Formula αThe equality of two terms as a first-order formula.
- Defined in
- Mathlib.ModelTheory.Syntax
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- FirstOrder.Language.Termstatement and proof · cited by 166
- FirstOrder.Language.Formulastatement · cited by 93
- FirstOrder.Language.Term.relabelproof · cited by 27
- FirstOrder.Language.Term.bdEqualproof · cited by 10
Cited by18
Results whose statement or proof uses this declaration.
- FirstOrder.Language.distinctConstantsTheoryproof · cited by 9
- FirstOrder.Language.Formula.graphproof · cited by 3
- FirstOrder.Field.eqZeroproof · cited by 3
- FirstOrder.Language.Term.definableFun_realizeproof · cited by 3
- FirstOrder.Language.Formula.iExsUniqueproof · cited by 2
- FirstOrder.Language.model_distinctConstantsTheoryproof · cited by 2
- FirstOrder.Ring.mvPolynomial_zeroLocus_definableproof · cited by 1
- FirstOrder.Language.distinctConstantsTheory_eq_iUnionproof · cited by 1
- IsLinearSet.definableproof · cited by 1
- Set.Definable.diagonalproof · cited by 1
- Set.Definable.image_compproof · cited by 1
- FirstOrder.Language.MeetsDefinable.closure_eq_selfproof · cited by 1