preimage_interior — Mathlib

English

For any subset s of Y, the preimage interior commutes with restriction: e.source ∩ e^{-1}(int s) = e.source ∩ int(e^{-1}(s)).

Русский

Для любой подмножества s пространства Y предобраз внутренности через e совпадает с внутренностью предобраза через e: e.source ∩ e^{-1}(int s) = e.source ∩ int(e^{-1}(s)).

LaTeX

$$$e.source \\cap e^{-1}(\\operatorname{int}\\,s) = e.source \\cap \\operatorname{int}(e^{-1}(s))$$$

Lean4

/-- Preimage of interior or interior of preimage coincide for open partial homeomorphisms,
when restricted to the source. -/
theorem preimage_interior (s : Set Y) : e.source ∩ e ⁻¹' interior s = e.source ∩ interior (e ⁻¹' s) :=
  (IsImage.of_preimage_eq rfl).interior.preimage_eq

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