English
In an OrderTopology α, for neighborhood s of a, there exist b,c with a ∈ Icc(b,c), Icc(b,c) a neighborhood of a, and Icc(b,c) ⊆ s.
Русский
В OrderTopology α для окрестности s точки a существуют b,c такие, что a ∈ Icc(b,c), Icc(b,c) — окрестность a и Icc(b,c) ⊆ s.
LaTeX
$$$\\exists b,c\\,\\ a\\in Icc(b,c)\\land Icc(b,c)\\in 𝓝 a \\land Icc(b,c)\\subseteq s$$$
Lean4
theorem exists_Icc_mem_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) :
∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s :=
by
rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with ⟨b, hba, hb_nhds, hbs⟩
rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with ⟨c, hac, hc_nhds, hcs⟩
refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]
exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩
