comp_isOpenMap_iff' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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