preAleph_max

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Cardinal.preAleph_max

English

preAleph distributes over maxima: preAleph(max(o1,o2)) = max(preAleph(o1), preAleph(o2)).

Русский

preAleph распределяет по максимуму: preAleph(max(o1,o2)) = max(preAleph(o1), preAleph(o2)).

LaTeX

$$$ \text{preAleph}(\max(o_1,o_2)) = \max(\text{preAleph}(o_1), \text{preAleph}(o_2)) $$$

Lean4

theorem preAleph_max (o₁ o₂ : Ordinal) : preAleph (max o₁ o₂) = max (preAleph o₁) (preAleph o₂) :=
  preAleph.monotone.map_max

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

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

Разделы

Аффилиация

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