isGLB_lt_isLUB_of_ne — Mathlib

English

If a is a GLB of s and b is an LUB of s with x,y ∈ s and x ≠ y, then a < b.

Русский

Если a — наибольший нижний предел s, b — наименьшая верхняя грань s, и существуют x,y ∈ s такие, что x ≠ y, тогда a < b.

LaTeX

$$IsGLB s a → IsLUB s b → ∀ {x y}, x ∈ s → y ∈ s → x ≠ y → a < b$$

Lean4

theorem isGLB_lt_isLUB_of_ne (Ha : IsGLB s a) (Hb : IsLUB s b) {x y} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) : a < b :=
  lt_iff_le_not_ge.2
    ⟨lowerBounds_le_upperBounds Ha.1 Hb.1 ⟨x, Hx⟩, fun hab => Hxy <| Set.subsingleton_of_isLUB_le_isGLB Ha Hb hab Hx Hy⟩

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