exists_ge — Mathlib

English

Let s be dense in α (a linear order with ClosedIicTopology). Then for every x ∈ α there exists y ∈ s with x ≤ y.

Русский

Пусть s плотно в α; тогда для каждого x ∈ α существует y ∈ s такой, что x ≤ y.

LaTeX

$$$[Dense\ s] \rightarrow \forall x:\, \alpha,\; \exists y \in s,\; x \le y$$$

Lean4

protected theorem exists_ge [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x ≤ y :=
  (hs.exists_gt x).imp fun _ h ↦ ⟨h.1, h.2.le⟩

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