bddBelow_coe — Mathlib

English

Let S be a subset of the nonnegative rationals. Then the image of S in the rationals, via the natural inclusion, is bounded below by 0.

Русский

Пусть S ⊆ ℚ≥0. Тогда образ S в ℚ под естественным включением ограничен снизу нулём.

LaTeX

$$$\forall S \subseteq \mathbb{Q}_{\ge 0},\quad BddBelow\Bigl(\{ s^{\uparrow} \mid s \in S \}\Bigr).$$$

Lean4

theorem bddBelow_coe (s : Set ℚ≥0) : BddBelow (((↑) : ℚ≥0 → ℚ) '' s) :=
  ⟨0, fun _ ⟨q, _, h⟩ ↦ h ▸ q.2⟩

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