exists_lt — Mathlib

English

If α has no minimum and s is dense in α, then for every x there exists y ∈ s with y < x.

Русский

Если у множества α нет минимума и s плотно относительно α, то для каждого x существует y ∈ s such that y < x.

LaTeX

$$$\text{NoMinOrder}(\alpha) \rightarrow \text{Dense}(s) \rightarrow \forall x \in α, \exists y \in s, y < x$$$

Lean4

protected theorem exists_lt [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y < x :=
  hs.orderDual.exists_gt x

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