isOpen_extend_preimage' — Mathlib

English

If s is open in E, then the intersection of the extended source with the preimage of s is open.

Русский

Если s открыто в E, то пересечение расширенного источника с прообразом s открыто.

LaTeX

$$$ IsOpen(s) \\Rightarrow IsOpen((f^{\\mathrm{extend}}_I).\\mathrm{source} \\cap (f^{\\mathrm{extend}}_I)^{-1}[s]). $$$

Lean4

theorem isOpen_extend_preimage' {s : Set E} (hs : IsOpen s) : IsOpen ((f.extend I).source ∩ f.extend I ⁻¹' s) :=
  (continuousOn_extend f).isOpen_inter_preimage (isOpen_extend_source _) hs

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