bddBelow_bddAbove_iff_subset_Icc — Mathlib

English

A set is bounded below and above if and only if it is contained in some closed interval [a,b].

Русский

Множество ограничено снизу и сверху тогда и только тогда, когда оно содержится внутри некоторого замкнутого интервала [a,b].

LaTeX

$$$\mathrm{BddBelow}(s) \land \mathrm{BddAbove}(s) \iff \exists a \exists b, \, s \subseteq \mathrm{Icc}(a,b).$$$

Lean4

theorem bddBelow_bddAbove_iff_subset_Icc : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b := by
  simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici, bddAbove_iff_subset_Iic, exists_and_left,
    exists_and_right]

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