open_dom_of_pcontinuous — Mathlib

English

If f is PContinuous, then the domain of f is open in X.

Русский

Если f — частичное отображение, непрерывное в смысле PContinuous, то область определения f открыта в X.

LaTeX

$$$\\text{PContinuous}(f) \\Rightarrow \\mathrm{IsOpen}(f\\mathrm{.Dom})$$$

Lean4

theorem open_dom_of_pcontinuous {f : X →. Y} (h : PContinuous f) : IsOpen f.Dom := by rw [← PFun.preimage_univ];
  exact h _ isOpen_univ

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