residual_map_eq — Mathlib

English

Under a homeomorphism, the residual filter is preserved (maps to the residual on the target).

Русский

Переобразование пространства через гомеоморфизм сохраняет резидуальный фильтр: резидуал на левом пространстве переносится в резидуал на правом.

LaTeX

$$$ (\\\\operatorname{residual} \\\\alpha).map h = \\\\operatorname{residual} \\\\beta $$$

Lean4

theorem residual_map_eq (h : α ≃ₜ β) : (residual α).map h = residual β :=
  by
  refine le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)
  simp_rw [← preimage_symm]
  exact tendsto_residual_of_isOpenMap h.symm.continuous h.symm.isOpenMap

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