Theorems · Definition · logic and foundations
FirstOrder.Language.distinctConstantsTheory
(L : FirstOrder.Language) → {α : Type u'} → Set α → (L.withConstants α).TheoryA theory indicating that each of a set of constants is distinct.
- Defined in
- Mathlib.ModelTheory.Syntax
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.imageproof · cited by 5,609
- Compl.complproof · cited by 2,925
- SProd.sprodproof · cited by 1,750
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Theorystatement · cited by 154
- FirstOrder.Language.withConstantsstatement · cited by 108
- Set.diagonalproof · cited by 42
- FirstOrder.Language.Formula.notproof · cited by 27
- FirstOrder.Language.conproof · cited by 21
- FirstOrder.Language.Term.equalproof · cited by 14
- FirstOrder.Language.Constants.termproof · cited by 11
Cited by9
Results whose statement or proof uses this declaration.
- FirstOrder.Language.model_distinctConstantsTheorystatement · cited by 2
- FirstOrder.Language.monotone_distinctConstantsTheorystatement · cited by 2
- FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_lestatement and proof · cited by 1
- FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinitestatement and proof · cited by 1
- FirstOrder.Language.distinctConstantsTheory_eq_iUnionstatement · cited by 1
- FirstOrder.Language.distinctConstantsTheory_monostatement · cited by 1
- FirstOrder.Language.card_le_of_model_distinctConstantsTheorystatement and proof · cited by 1
- FirstOrder.Language.Theory.exists_large_model_of_infinite_modelproof · cited by 1
- FirstOrder.Language.directed_distinctConstantsTheorystatement · cited by 0