respectsIso — Mathlib

English

The dominant property is invariant under isomorphisms of morphisms: if f ≅ f', then IsDominant f ⇔ IsDominant f'.

Русский

Свойство доминирующего отображения сохраняется при изоморфизмах морфизмов: если f изоморфен f', то IsDominant f ⇔ IsDominant f'.

LaTeX

$$$(\\mathrm{IsDominant})$ respects isomorphisms$$

Lean4

instance respectsIso : MorphismProperty.RespectsIso @IsDominant :=
  MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ f (_ : IsIso f) ↦ inferInstance

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