English
Let s be dense in α. If for every top element x we have x ∈ s, then for every x ∈ α there exists y ∈ s with x ≤ y.
Русский
Пусть s плотное множество; если для каждого верхнего элемента x выполняется x ∈ s, то для каждого x ∈ α существует y ∈ s такой, что x ≤ y.
LaTeX
$$$(\text{Dense } s) \rightarrow (\forall x, \ IsTop(x) \rightarrow x \in s) \rightarrow \forall x:\, \alpha,\; \exists y \in s,\; x \le y$$$
Lean4
theorem exists_ge' {s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) : ∃ y ∈ s, x ≤ y :=
by
by_cases hx : IsTop x
· exact ⟨x, htop x hx, le_rfl⟩
· simp only [IsTop, not_forall, not_le] at hx
rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩
exact ⟨y, hys, hy.le⟩
