isOpen_extChartAt_preimage' — Mathlib

English

If s is open in the model space, then the preimage of s under extChartAt x is open when intersected with the source.

Русский

Если s открыто в пространстве модели, то прообраз под extChartAt x пересеченный с областью определения открыт.

LaTeX

$$$$ \text{IsOpen}\bigl((\text{extChartAt } I x)\text{ source} \cap (\text{extChartAt } I x)^{-1}(s)\bigr). $$$$

Lean4

theorem isOpen_extChartAt_preimage' (x : M) {s : Set E} (hs : IsOpen s) :
    IsOpen ((extChartAt I x).source ∩ extChartAt I x ⁻¹' s) :=
  isOpen_extend_preimage' _ hs

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