bddAbove_coe — Mathlib

English

Bounding above is preserved by coercion: BddAbove (↑'' s) in ℚ is equivalent to BddAbove s in ℚ≥0.

Русский

Предел выше сохраняется через приведение: BddAbove (↑'' s) в ℚ эквивалентно BddAbove s в ℚ≥0.

LaTeX

$$$$ BddAbove (\uparrow '' s) \;\text{ в } \mathbb{Q} \iff BddAbove\; s. $$$$

Lean4

theorem bddAbove_coe {s : Set ℚ≥0} : BddAbove ((↑) '' s : Set ℚ) ↔ BddAbove s :=
  ⟨fun ⟨b, hb⟩ ↦
    ⟨toNNRat b, fun ⟨y, _⟩ hys ↦ show y ≤ max b 0 from (hb <| Set.mem_image_of_mem _ hys).trans <| le_max_left _ _⟩,
    fun ⟨b, hb⟩ ↦ ⟨b, fun _ ⟨_, hx, Eq⟩ ↦ Eq ▸ hb hx⟩⟩

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