isBoundedUnder_ge_toReal — Mathlib

English

IsBoundedUnder (≥) for NNReal corresponds to IsBoundedUnder (≥) after toReal.

Русский

IsBoundedUnder (≥) для NNReal эквивалентно IsBoundedUnder (≥) после toReal.

LaTeX

$$$\mathrm{IsBoundedUnder}(\ge)\ f\; (u) \iff \mathrm{IsBoundedUnder}(\ge)\ f\; u.$$$

Lean4

@[simp, norm_cast]
theorem isBoundedUnder_ge_toReal : IsBoundedUnder (· ≥ ·) f (fun i ↦ (u i : ℝ)) ↔ IsBoundedUnder (· ≥ ·) f u :=
  by
  simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, by simpa⟩
  · rintro ⟨b, -, hb⟩
    exact ⟨b, hb⟩

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