isCoboundedUnder_le_toReal — Mathlib

English

IsCoboundedUnder (≤) f (u) is equivalent to IsCoboundedUnder (≤) f u via the Real realization.

Русский

IsCoboundedUnder (≤) f (u) эквивалентно IsCoboundedUnder (≤) f u через переход к Real.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem isCoboundedUnder_le_toReal [f.NeBot] :
    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.toNNReal, by simp, fun x _ ↦ by simpa [*] using hb _⟩
  · rintro ⟨b, hb₀, hb⟩
    exact ⟨b, fun x hx ↦ hb _ (hx.exists.choose_spec.trans' (by simp)) hx⟩

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