subsingleton_of_isLUB_le_isGLB — Mathlib

English

Let Ha be a GLB of s with a, Hb be a LUB of s with b, and assume b ≤ a. Then s is subsingleton (has at most one element).

Русский

Пусть a — наибольший нижний предел s, b — наименьший верхний предел s, и пусть b ≤ a. Тогда s содержит не более одного элемента.

LaTeX

$$(IsGLB s a) → (IsLUB s b) → b ≤ a → s.Subsingleton$$

Lean4

theorem subsingleton_of_isLUB_le_isGLB (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : s.Subsingleton :=
  fun _ hx _ hy => le_antisymm (le_of_isLUB_le_isGLB Ha Hb hab hx hy) (le_of_isLUB_le_isGLB Ha Hb hab hy hx)

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