lt_isLUB_iff — Mathlib

English

Let s be a set in a linear order and a its LUB. Then for any b, b < a if and only if there exists c ∈ s with b < c.

Русский

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

LaTeX

$$$ IsLUB(s,a) \\rightarrow (b < a \\leftrightarrow \\exists c \\in s, b < c)$$$

Lean4

theorem lt_isLUB_iff (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c := by
  simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]

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