inf — Mathlib

English

If P and Q are stable under base change, then their infimum P ⊓ Q is stable under base change.

Русский

Если P и Q стабильны относительно базового изменения, то их инфимума (P ⊓ Q) стабилен.

LaTeX

$$$[P.IsStableUnderBaseChange] \land [Q.IsStableUnderBaseChange] \Rightarrow [(P \sqcap Q).IsStableUnderBaseChange]$$$

Lean4

instance inf {P Q : MorphismProperty C} [IsStableUnderBaseChange P] [IsStableUnderBaseChange Q] :
    IsStableUnderBaseChange (P ⊓ Q) where of_isPullback hp hg := ⟨of_isPullback hp hg.left, of_isPullback hp hg.right⟩

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