exists_gt — Mathlib

English

Let s be a dense subset of a linear order α with no maximum. Then for every x ∈ α there exists y ∈ s with x < y.

Русский

Пусть s — плотное подмножество линейного порядка α без максимума. Тогда для каждого x ∈ α существует y ∈ s такое, что x < y.

LaTeX

$$$[NoMaxOrder \ α] \; {s : Set \ α} \rightarrow (\text{Dense } s) \rightarrow \forall x:\, α,\; \exists y \in s,\; x < y$$$

Lean4

protected theorem exists_gt [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x < y :=
  hs.exists_mem_open isOpen_Ioi (exists_gt x)

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