isBoundedUnder_le_toReal — Mathlib

English

IsBoundedUnder (≤) for NNReal corresponds to IsBounded (≤) after passing toReal.

Русский

IsBoundedUnder (≤) для NNReal эквивалентно IsBounded (≤) после приведения к Real.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem isBoundedUnder_le_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 filter_upwards [hb]; simp +contextual⟩
  · rintro ⟨b, -, hb⟩
    exact ⟨b, hb⟩

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