comap_toNNReal_atTop — Mathlib

English

comap Real.toNNReal atTop = atTop.

Русский

Обратное отображение Real.toNNReal к atTop совпадает с atTop.

LaTeX

$$$comap Real.toNNReal atTop = atTop$$$

Lean4

@[simp]
theorem _root_.Real.comap_toNNReal_atTop : comap Real.toNNReal atTop = atTop :=
  by
  refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap
  refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_
  filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx
  exact (Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx

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