isCoboundedUnder_ge_toReal — Mathlib

English

IsCoboundedUnder (≥) f (u) is equivalent to IsCoboundedUnder (≥) f u via toReal.

Русский

IsCoboundedUnder (≥) f (u) эквивалентно IsCoboundedUnder (≥) f u через toReal.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem isCoboundedUnder_ge_toReal : IsCoboundedUnder (· ≥ ·) f (fun i ↦ (u i : ℝ)) ↔ IsCoboundedUnder (· ≥ ·) f u :=
  by
  simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall, NNReal.exists]
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨b, hb _ (by simp), fun x _ ↦ hb _⟩
  · rintro ⟨b, hb₀, hb⟩
    refine ⟨b, fun x hx ↦ ?_⟩
    obtain hx₀ | hx₀ := le_total x 0
    · exact hx₀.trans hb₀
    · exact hb _ hx₀ hx

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