Theorems · Definition · logic and foundations
FirstOrder.Language.Term.bdEqual
{L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α nThe equality of two terms as a bounded formula.
- Defined in
- Mathlib.ModelTheory.Syntax
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 3 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
- FirstOrder.Language.BoundedFormulastatement · cited by 207
- FirstOrder.Language.Termstatement and proof · cited by 166
Cited by18
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Term.equalproof · cited by 14
- FirstOrder.Field.genericMonicPolyHasRootproof · cited by 4
- FirstOrder.genericPolyMapSurjOnOfInjOnproof · cited by 4
- FirstOrder.Language.Sentence.cardGeproof · cited by 3
- FirstOrder.Language.BoundedFormula.IsAtomic.recOnstatement and proof · cited by 3
- FirstOrder.Language.BoundedFormula.IsAtomic.casesOnstatement and proof · cited by 2
- FirstOrder.Language.Relations.antisymmetricproof · cited by 2
- FirstOrder.realize_genericPolyMapSurjOnOfInjOnproof · cited by 2
- FirstOrder.Ring.mvPolynomial_zeroLocus_definableproof · cited by 1
- FirstOrder.Field.FieldAxiom.toSentenceproof · cited by 1
- FirstOrder.Language.BoundedFormula.not_all_isAtomicproof · cited by 1
- FirstOrder.Language.BoundedFormula.not_ex_isAtomicproof · cited by 1