nonempty

Mathlib.ModelTheory.Semantics

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementarilyEquivalent.nonempty

English

Infinite property is preserved under elementary equivalence.

Русский

Если M эквивалентна N по L, то M бесконечно тогда и только тогда, когда N бесконечна.

LaTeX

$$M ≅_L N → (Infinite(M) ↔ Infinite(N))$$

Lean4

theorem nonempty [Mn : Nonempty M] (h : M ≅[L] N) : Nonempty N :=
  h.nonempty_iff.1 Mn

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

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

Разделы

Аффилиация

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