comp_isOpenMap_iff — Mathlib

English

For a homeomorphism h: X ≃ₜ Y and any f: Z → X, IsOpenMap (h ∘ f) ↔ IsOpenMap f.

Русский

Для гомеоморфизма h: X ≃ₜ Y и любой функции f: Z → X выполняется IsOpenMap (h ∘ f) ⇔ IsOpenMap f.

LaTeX

$$$IsOpenMap(h \circ f) \iff IsOpenMap(f).$$$

Lean4

@[simp]
theorem comp_isOpenMap_iff (h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (h ∘ f) ↔ IsOpenMap f :=
  by
  refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩
  intro hf
  rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]
  exact h.symm.isOpenMap.comp hf

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