bdd_below_bdd_above_iff_subset_uIcc

English

A set s is bounded below and above if and only if there exist a, b with s ⊆ [[a, b]].

Русский

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

LaTeX

$$$ BddBelow\\, s \\land BddAbove\\, s \\\\iff \\Exists a \\Exists b, s \\subseteq [[a,b]] $$$

Lean4

theorem bdd_below_bdd_above_iff_subset_uIcc (s : Set α) : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ [[a, b]] :=
  bddBelow_bddAbove_iff_subset_Icc.trans
    ⟨fun ⟨a, b, h⟩ => ⟨a, b, fun _ hx => Icc_subset_uIcc (h hx)⟩, fun ⟨_, _, h⟩ => ⟨_, _, h⟩⟩

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