age_eq_age

Mathlib.ModelTheory.Fraisse

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Equiv.age_eq_age

English

If M ≃ N, then the ages are equal: L.age M = L.age N.

Русский

Если M и N изоморфны, то их возраста совпадают: L.age M = L.age N.

LaTeX

$$$(M \cong_L N) \Rightarrow L.\mathrm{age}(M) = L.\mathrm{age}(N)$$$

Lean4

theorem age_eq_age (MN : M ≃[L] N) : L.age M = L.age N :=
  le_antisymm MN.toEmbedding.age_subset_age MN.symm.toEmbedding.age_subset_age

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

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

Разделы

Аффилиация

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