exists_Icc_mem_subset_of_mem_nhdsLE

English

In an OrderTopology α, for a neighborhood within the ≤-ray, there exists b≤a such that Icc(b,a) is a neighborhood within that ray and Icc(b,a) ⊆ s.

Русский

В OrderTopology α для окрестности в направлении ≤ существует b≤a, такое что Icc(b,a) — окрестность и Icc(b,a) ⊆ s.

LaTeX

$$$\\exists b\\le a,\\ Icc(b,a)\\in 𝓝_{[≤]} a \\land Icc(b,a) \\subseteq s$$$

Lean4

theorem exists_Icc_mem_subset_of_mem_nhdsLE [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝[≤] a) :
    ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s := by
  simpa only [Icc_toDual, toDual.surjective.exists] using
    exists_Icc_mem_subset_of_mem_nhdsGE (α := αᵒᵈ) (a := toDual a) hs

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