bddAbove_coe — Mathlib

English

A set image under the inclusion is bounded above in ℝ if and only if the original set is bounded above in ℝ≥0.

Русский

Образ множества через включение ограничен сверху в ℝ тогда и только тогда, когда исходное множество ограничено сверху в ℝ≥0.

LaTeX

$$$ BddAbove\\left( (\\uparrow) '' s \\right) \\iff BddAbove\\, s $.$$

Lean4

theorem bddAbove_coe {s : Set ℝ≥0} : BddAbove (((↑) : ℝ≥0 → ℝ) '' s) ↔ BddAbove s :=
  Iff.intro
    (fun ⟨b, hb⟩ =>
      ⟨Real.toNNReal b, fun ⟨y, _⟩ hys => show y ≤ max b 0 from le_max_of_le_left <| hb <| Set.mem_image_of_mem _ hys⟩)
    fun ⟨b, hb⟩ => ⟨b, fun _ ⟨_, hx, eq⟩ => eq ▸ hb hx⟩

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