isHomeomorph_precomp — Mathlib

English

For any morphism f: A ⟶ B, if f is an isomorphism, then the precomposition map (f ≫ ·): (B ⟶ R) → (A ⟶ R) is a homeomorphism.

Русский

Для любой морфизм A ⟶ B, если он изоморфизм, то предосогласование (f ≫ ·) является гомеоморфизмом между Hom(B,R) и Hom(A,R).

LaTeX

$$$[IsIso\,f] \Rightarrow \text{IsHomeomorph}\big((f ≫ \cdot): (B \to R) \to (A \to R)\big)$$$

Lean4

theorem isHomeomorph_precomp (f : A ⟶ B) [IsIso f] : IsHomeomorph ((f ≫ ·) : (B ⟶ R) → (A ⟶ R)) :=
  (precompHomeomorph (asIso f)).isHomeomorph

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