preAleph_le_of_strictMono — Mathlib

English

If f is strictly increasing, then for all o, preAleph(o) ≤ f(o).

Русский

Если f строго возрастает, тогда для каждого o выполняется preAleph(o) ≤ f(o).

LaTeX

$$$$ \forall {f: \mathrm{Ordinal} \to \mathrm{Cardinal}}, \mathrm{StrictMono}(f) \rightarrow \forall o:\mathrm{Ordinal}, \operatorname{preAleph}(o) \le f(o). $$$$

Lean4

theorem preAleph_le_of_strictMono {f : Ordinal → Cardinal} (hf : StrictMono f) (o : Ordinal) : preAleph o ≤ f o := by
  simpa using (hf.comp preAleph.symm.strictMono).id_le (preAleph o)

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