instIsMultiplicativeSchemeIsDominant

English

Dominant morphisms are closed under composition: if f and g are dominant, then f ≫ g is dominant.

Русский

Доминантные морфизмы замкнуты по композиции: если f и g доминируют, то f ≫ g доминирует.

LaTeX

$$$\\mathrm{IsDominant}(f) \\land \\mathrm{IsDominant}(g) \\Rightarrow \\mathrm{IsDominant}(f \\circ g)$$$

Lean4

instance : MorphismProperty.IsMultiplicative @IsDominant
    where
  id_mem := fun _ ↦ inferInstance
  comp_mem := fun _ _ _ _ ↦ inferInstance

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