bddBelow_coe

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.bddBelow_coe

English

The image of a set under the inclusion is bounded below; in fact, 0 is a lower bound.

Русский

Образ множества через включение ограничен снизу; фактически 0 является нижней гранью.

LaTeX

$$$ BddBelow ( (\\uparrow) '' s ). $$$

Lean4

theorem bddBelow_coe (s : Set ℝ≥0) : BddBelow (((↑) : ℝ≥0 → ℝ) '' s) :=
  ⟨0, fun _ ⟨q, _, eq⟩ => eq ▸ q.2⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru