Theorems · Definition · logic and foundations
FirstOrder.Language.ElementarilyEquivalent
(L : FirstOrder.Language) → (M : Type w) → (N : Type u_1) → [L.Structure M] → [L.Structure N] → Prop
Two structures are elementarily equivalent when they satisfy the same sentences.
- Defined in
- Mathlib.ModelTheory.Semantics
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses Quot.sound
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.Structurestatement and proof · cited by 775
- FirstOrder.Language.completeTheoryproof · cited by 14
Cited by20
Results whose statement or proof uses this declaration.
- FirstOrder.Language.elementarilyEquivalent_iffstatement · cited by 4
- FirstOrder.Language.ElementarilyEquivalent.theory_model_iffstatement and proof · cited by 3
- Cardinal.Categorical.isCompleteproof · cited by 3
- FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalentstatement · cited by 2
- FirstOrder.Language.exists_elementarilyEquivalent_card_eqstatement · cited by 2
- FirstOrder.Language.ElementarilyEquivalent.completeTheory_eqstatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.infinite_iffstatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.nonemptystatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.nonempty_iffstatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.realize_sentencestatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.symmstatement and proof · cited by 1
- FirstOrder.Language.ElementarilyEquivalent.theory_modelstatement and proof · cited by 1