eq_univ_of_unbounded — Mathlib

English

A preconnected subset of a linear order that is unbounded below and above must be the whole space.

Русский

Предсвязное подмножество линейного порядка, не ограниченное снизу и сверху, равно всей области.

LaTeX

$$$\text{IsPreconnected}(s) \land \neg BddBelow(s) \land \neg BddAbove(s) \Rightarrow s = \mathrm{univ}$$$

Lean4

/-- If preconnected set in a linear order space is unbounded below and above, then it is the whole
space. -/
theorem eq_univ_of_unbounded {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : ¬BddAbove s) : s = univ :=
  by
  refine eq_univ_of_forall fun x => ?_
  obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x
  obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
  exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

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