exists_Ioc_subset_of_mem_nhds' — Mathlib

English

Same as above, expressed via dual order to obtain a variant for Ioc(l,a).

Русский

То же утверждение в случае двойственного порядка для получения варианта Ioc(l,a).

LaTeX

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

Lean4

theorem exists_Ioc_subset_of_mem_nhds' [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {l : α} (hl : l < a) :
    ∃ l' ∈ Ico l a, Ioc l' a ⊆ s :=
  let ⟨l', hl'a, hl's⟩ := exists_Ioc_subset_of_mem_nhds hs ⟨l, hl⟩
  ⟨max l l', ⟨le_max_left _ _, max_lt hl hl'a⟩, (Ioc_subset_Ioc_left <| le_max_right _ _).trans hl's⟩

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