StableUnderComposition — Mathlib

English

A property P is stable under composition if whenever f and g satisfy P, their composition g ∘ f also satisfies P.

Русский

Свойство P устойчиво к композиции, если при наличии f и g с свойством P, композиция g ∘ f также удовлетворяет P.

LaTeX

$$$\text{StableUnderComposition}(P) := \forall R,S,T, \forall f:R\to S, g:S\to T, P(f) \wedge P(g) \Rightarrow P(g\circ f).$$$

Lean4

/-- A property is `StableUnderComposition` if the composition of two such morphisms
still falls in the class. -/
def StableUnderComposition : Prop :=
  ∀ ⦃R S T⦄ [CommRing R] [CommRing S] [CommRing T], ∀ (f : R →+* S) (g : S →+* T) (_ : P f) (_ : P g), P (g.comp f)

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