English
In an OrderTopology α, for a neighborhood s of a within the ≥-ray, there exists b≥a such that Icc(a,b) is a neighborhood of a within that ray and Icc(a,b) ⊆ s.
Русский
В OrderTopology α для окрестности s в направлении ≥ существует b≥a, такое что Icc(a,b) — окрестность a и Icc(a,b) ⊆ s.
LaTeX
$$$\\exists b\\ge a,\\ Icc(a,b)\\in 𝓝_{[≥]} a \\land Icc(a,b) \\subseteq s$$$
Lean4
theorem exists_Icc_mem_subset_of_mem_nhdsGE [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝[≥] a) :
∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s :=
by
rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
· use a
simpa [ha.Ici_eq] using hs
· rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩)
· have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩
· refine ⟨c, hac.le, Icc_mem_nhdsGE hac, ?_⟩
exact (Icc_subset_Ico_right hcb).trans hbs
