bijective_of_isIso

Mathlib.CategoryTheory.ConcreteCategory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ConcreteCategory.bijective_of_isIso

English

If f is an isomorphism, then the underlying function f is bijective.

Русский

Если f является изоморфизмом, то его базовая функция биективна.

LaTeX

$$$\\text{IsIso}(f) \\Rightarrow \\text{Bijective}(\\underline{f})$$$

Lean4

theorem bijective_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] : Function.Bijective f :=
  by
  rw [← isIso_iff_bijective]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru