preAleph_le_preAleph — Mathlib

English

preAleph preserves order with respect to ≤: preAleph o1 ≤ preAleph o2 iff o1 ≤ o2.

Русский

preAleph сохраняет порядок относительно ≤: preAleph o1 ≤ preAleph o2 тогда и только тогда, когда o1 ≤ o2.

LaTeX

$$$ \text{preAleph}(o_1) \le \text{preAleph}(o_2) \iff o_1 \le o_2 $$$

Lean4

theorem preAleph_le_preAleph {o₁ o₂ : Ordinal} : preAleph o₁ ≤ preAleph o₂ ↔ o₁ ≤ o₂ :=
  preAleph.le_iff_le

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