stableUnderComposition — Mathlib

English

If f: X → Y and g: Y → Z are morphisms with IsProper f and IsProper g, then the composition f ≫ g is IsProper.

Русский

Если морфизмы f: X → Y и g: Y → Z имеют свойство IsProper, то композиция f ≫ g тоже является IsProper.

LaTeX

$$$[\text{IsProper } f] \land [\text{IsProper } g] \Rightarrow \text{IsProper}(f \circ g)$$$

Lean4

instance stableUnderComposition : MorphismProperty.IsStableUnderComposition @IsProper :=
  by
  rw [isProper_eq]
  infer_instance

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