universallyClosed_isStableUnderComposition

English

UniversallyClosed is stable under composition: if f and g are universally closed, then f ≫ g is universally closed.

Русский

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

LaTeX

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

Lean4

instance universallyClosed_isStableUnderComposition : IsStableUnderComposition @UniversallyClosed :=
  by
  rw [universallyClosed_eq]
  infer_instance

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