exists_between' — Mathlib

English

If a is the LUB of s and a ∉ s and hb: b < a, then there exists c ∈ s with b < c ∧ c < a.

Русский

Если a — наименьшая верхняя грань s, а a ∉ s и b < a, то существует c ∈ s такое, что b < c < a.

LaTeX

$$IsLUB s a → Not (a ∈ s) → b < a → ∃ c ∈ s, b < c ∧ c < a$$

Lean4

theorem exists_between' (h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a :=
  let ⟨c, hcs, hbc, hca⟩ := h.exists_between hb
  ⟨c, hcs, hbc, hca.lt_of_ne fun hac => h' <| hac ▸ hcs⟩

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