exists_le — 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 с y ≤ x.

LaTeX

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

Lean4

protected theorem exists_le [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y ≤ x :=
  hs.orderDual.exists_ge x

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