exists_Ioo_subset — Mathlib

English

If s is open in an OrderTopology α and s is nonempty, there exist a,b with a<b and Ioo(a,b) ⊆ s.

Русский

Пусть s открыто в OrderTopology α и непусто; тогда существуют a<b такие, что Ioo(a,b) ⊆ s.

LaTeX

$$$\\exists a,b\\ (a

Lean4

theorem exists_Ioo_subset [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) :
    ∃ a b, a < b ∧ Ioo a b ⊆ s := by
  obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h
  obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x
  rcases lt_trichotomy x y with (H | rfl | H)
  · obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s := exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩
  · exact (hy rfl).elim
  · obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s := exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩

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