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⟩⟩