inf — Mathlib

English

The infimum of two stable-under-composition properties is stable under composition, with comp_mem given componentwise.

Русский

Наименьшее сверху двух свойств, устойчивых к композиции, сохраняет устойчивость к композиции; составление определяется компонентно.

LaTeX

$$IsStableUnderComposition inf$$

Lean4

instance inf {P Q : MorphismProperty C} [P.IsStableUnderComposition] [Q.IsStableUnderComposition] :
    (P ⊓ Q).IsStableUnderComposition where
  comp_mem f g hf hg := ⟨P.comp_mem f g hf.left hg.left, Q.comp_mem f g hf.right hg.right⟩

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