dirSupInaccOn_of_isOpen — Mathlib

English

If s is open in a Scott–Hausdorff space, then DirSupInaccOn D s holds.

Русский

Если s открыто в пространстве Скотт–Хаусдорфа, то DirSupInaccOn D s выполняется.

LaTeX

$$$\\text{IsOpen}(s) \\Rightarrow \\text{DirSupInaccOn}(D,s)$$$

Lean4

theorem dirSupInaccOn_of_isOpen [IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s :=
  fun d hd₀ hd₁ hd₂ a hda hd₃ ↦ by obtain ⟨b, hbd, hb⟩ := isOpen_iff.mp h hd₀ hd₁ hd₂ hda hd₃;
  exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

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