relative_monotone — Mathlib

English

If P ≤ P' as morphism properties on C, then P.relative F ≤ P'.relative F; i.e., relative properties inherit monotonicity along P → P'.

Русский

Если P ≤ P', то P.relative F ≤ P'.relative F; относительные свойства сохраняют монотонность.

LaTeX

$$$P \le P' \Rightarrow P.relative F \le P'.relative F$$$

Lean4

/-- If `P' : MorphismProperty C` is satisfied whenever `P` is, then also `P'.relative` is
satisfied whenever `P.relative` is. -/
theorem relative_monotone {P' : MorphismProperty C} (h : P ≤ P') : P.relative F ≤ P'.relative F := fun _ _ _ hf ↦
  ⟨hf.rep, fun _ _ g fst snd BC ↦ h _ (hf.property g fst snd BC)⟩

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