limitsOfShape_monotone — Mathlib

English

If W₁ ≤ W₂ then W₁.limitsOfShape J ≤ W₂.limitsOfShape J for any shape J.

Русский

Если W₁ ≤ W₂, то W₁.limitsOfShape J ≤ W₂.limitsOfShape J для любой формы J.

LaTeX

$$$W_1 \le W_2 \Rightarrow W_1.limitsOfShape J \le W_2.limitsOfShape J$$$

Lean4

theorem limitsOfShape_monotone {W₁ W₂ : MorphismProperty C} (h : W₁ ≤ W₂) (J : Type*) [Category J] :
    W₁.limitsOfShape J ≤ W₂.limitsOfShape J :=
  by
  rintro _ _ _ ⟨_, _, _, _, h₁, _, f, hf⟩
  exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

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