toENat_strictMonoOn — Mathlib

English

The map toENat is strictly monotone on the interval up to aleph-null: on the set Iic(ℵ0), toENat is strictly monotone.

Русский

Отображение toENat строго монотонно на интервале до ℵ0: на множестве Iic(ℵ0).

LaTeX

$$$\\operatorname{StrictMonoOn}(\\operatorname{toENat}, \\mathrm{Iic}(\\aleph_0))$$$

Lean4

theorem toENat_strictMonoOn : StrictMonoOn toENat (Iic ℵ₀) :=
  by
  simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]
  exact fun _ _ ↦ id

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