mul_omega0

Mathlib.SetTheory.Ordinal.Principal

URI: https://scilib.ai/kg/mathlib#Ordinal.mul_omega0

English

If 0 < a and a < ω, then a * ω = ω.

Русский

Если 0 < a и a < ω, то a * ω = ω.

LaTeX

$$$(0 < a) \land (a < \omega) \Rightarrow a * \omega = \omega.$$$

Lean4

theorem mul_omega0 (a0 : 0 < a) (ha : a < ω) : a * ω = ω :=
  principal_mul_iff_mul_left_eq.1 principal_mul_omega0 a a0 ha

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

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

Разделы

Аффилиация

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