quasiSeparated_isStableUnderComposition

English

Quasi-separatedness (as a morphism property) is stable under composition: if f and g are quasi-separated, then g ∘ f is quasi-separated.

Русский

Квазисепарабельность как свойство морфизма устойчиво к композиции: если f и g квазисепарактны, то g ∘ f тоже квазисепарактен.

LaTeX

$$$\\text{QuasiSeparated}(f) \\land \\text{QuasiSeparated}(g) \\Rightarrow \\text{QuasiSeparated}(g \\circ f)$$$

Lean4

instance quasiSeparated_isStableUnderComposition : MorphismProperty.IsStableUnderComposition @QuasiSeparated :=
  quasiSeparated_eq_diagonal_is_quasiCompact.symm ▸ inferInstance

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