exists_Ico_subset_of_mem_nhds' — Mathlib

English

In an OrderTopology α, for a neighborhood of a and u with a < u, there exists u' with a < u' ≤ u and Ico(a,u') ⊆ s.

Русский

В OrderTopology α для окрестности a и элемента u> a существует u' с a < u' ≤ u и Ico(a,u') ⊆ s.

LaTeX

$$$\\forall a\\in α,\\forall s\\subseteq α\\,(s\\in 𝓝 a)\\Rightarrow \\exists u'\\in Ioc(a,u), Ico(a,u')\\subseteq s$$$

Lean4

theorem exists_Ico_subset_of_mem_nhds' [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {u : α} (hu : a < u) :
    ∃ u' ∈ Ioc a u, Ico a u' ⊆ s := by
  simpa only [OrderDual.exists, exists_prop, Ico_toDual, Ioc_toDual] using
    exists_Ioc_subset_of_mem_nhds' (show ofDual ⁻¹' s ∈ 𝓝 (toDual a) from hs) hu.dual

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