exists_between — Mathlib

English

If h : IsGLB s a and hb : a < b, then there exists c ∈ s with a ≤ c ∧ c < b.

Русский

Если a является наибольшей нижней границей s и a < b, то существует c ∈ s такое, что a ≤ c и c < b.

LaTeX

$$IsGLB s a → a < b → ∃ c ∈ s, a ≤ c ∧ c < b$$

Lean4

theorem exists_between (h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b :=
  let ⟨c, hcs, hbc⟩ := (isGLB_lt_iff h).1 hb
  ⟨c, hcs, h.1 hcs, hbc⟩

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