forget_reflectsIsomorphisms — Mathlib

English

The forgetful functor from CompHausLike P to TopCat reflects isomorphisms: if a morphism has an underlying bijective map, then it is an isomorphism in CompHausLike.

Русский

Функтор забывания из CompHausLike P в TopCat отражает изоморфизмы: если морфизм имеет биективное подлежащие отображение, то он является изоморфизмом в CompHausLike.

LaTeX

$$$ \\forall X,Y \\in \\text{CompHausLike }P,\\; \\forall f:X\\to Y,\\; \\operatorname{Bijective}(\\underline{f})\\Rightarrow f\\text{ is an isomorphism}$$$

Lean4

instance forget_reflectsIsomorphisms : (forget (CompHausLike.{u} P)).ReflectsIsomorphisms :=
  ⟨by intro A B f hf; rw [isIso_iff_bijective] at hf; exact isIso_of_bijective _ hf⟩

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