beth_le_beth

Mathlib.SetTheory.Cardinal.Aleph

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

English

Beth is order-embedded in the sense that beth(o1) ≤ beth(o2) iff o1 ≤ o2.

Русский

Beth сохраняет порядок вплоть до эквивалентности: beth(o1) ≤ beth(o2) если и только если o1 ≤ o2.

LaTeX

$$$\beth(o_1) \le \beth(o_2) \iff o_1 \le o_2$$$

Lean4

@[simp]
theorem beth_le_beth {o₁ o₂ : Ordinal} : ℶ_ o₁ ≤ ℶ_ o₂ ↔ o₁ ≤ o₂ :=
  beth_strictMono.le_iff_le

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

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

Разделы

Аффилиация

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