strictLimitsOfShape_monotone — Mathlib

English

If P is contained in Q as a property on a category C, then for any shape J, the strict limits of shape J for P are contained in the strict limits of shape J for Q.

Русский

Пусть P является подмножество свойств на категории C и P ⊆ Q. Тогда для любого множества форм внутри формы J строгие пределы для P вложены в строгие пределы для Q: P.strictLimitsOfShape(J) ≤ Q.strictLimitsOfShape(J).

LaTeX

$$$P\mathrm{.strictLimitsOfShape}(J) \le Q\mathrm{.strictLimitsOfShape}(J)$$$

Lean4

theorem strictLimitsOfShape_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
    P.strictLimitsOfShape J ≤ Q.strictLimitsOfShape J :=
  by
  rintro _ ⟨F, hF⟩
  exact ⟨F, fun j ↦ h _ (hF j)⟩

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