elementarilyEquivalent

Mathlib.ModelTheory.ElementaryMaps

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent

English

If f is an elementary embedding between M and N, then M and N are elementarily equivalent.

Русский

Если имеется элементарное вложение между M и N, то они элементарно эквивалентны.

LaTeX

$$$M \cong_L N$$$

Lean4

theorem elementarilyEquivalent (f : M ↪ₑ[L] N) : M ≅[L] N :=
  elementarilyEquivalent_iff.2 f.map_sentence

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru