cof_le — Mathlib

English

For any normal f, cof a ≤ cof (f a).

Русский

Для любой нормальной f Cof(a) ≤ Cof(f(a)).

LaTeX

$$$$\operatorname{cof}(a) \le \operatorname{cof}(f(a)).$$$$

Lean4

theorem cof_le {f} (hf : IsNormal f) (a) : cof a ≤ cof (f a) :=
  by
  rcases zero_or_succ_or_isSuccLimit a with (rfl | ⟨b, rfl⟩ | ha)
  · rw [cof_zero]
    exact zero_le _
  · rw [cof_succ, Cardinal.one_le_iff_ne_zero, cof_ne_zero, ← Ordinal.pos_iff_ne_zero]
    exact (Ordinal.zero_le (f b)).trans_lt (hf.strictMono (lt_succ b))
  · rw [hf.cof_eq ha]

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