English
Elementary equivalence is transitive.
Русский
Если M эквивалентна как-то элементарно N, а N элементарно эквивалентна P, то и M элементарно эквивалентна P.
LaTeX
$$M ≡_L N ∧ N ≡_L P ⇒ M ≡_L P$$
Lean4
theorem model_distinctConstantsTheory {M : Type w} [L[[α]].Structure M] (s : Set α) :
M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i : α => (L.con i : M)) s :=
by
simp only [distinctConstantsTheory, Theory.model_iff, Set.mem_image, Prod.exists, forall_exists_index, and_imp]
refine ⟨fun h a as b bs ab => ?_, ?_⟩
· contrapose! ab
have h' := h _ a b ⟨⟨as, bs⟩, ab⟩ rfl
simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants] at h'
exact h'
· rintro h φ a b ⟨⟨as, bs⟩, ab⟩ rfl
simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]
exact fun contra => ab (h as bs contra)
