strictLimitsOfShape_le_limitsOfShape

English

For object property P, strictLimitsOfShape J is less or equal to limitsOfShape J; i.e., strict limits imply ordinary limits.

Русский

Для свойства объектов P строгие пределы формы J включают обычные пределы формы J; строгие пределы ⊆ пределы.

LaTeX

$$$P^{\text{strictLimitsOfShape}}(J) \le P^{\text{limitsOfShape}}(J)$$$

Lean4

theorem strictLimitsOfShape_le_limitsOfShape : P.strictLimitsOfShape J ≤ P.limitsOfShape J :=
  by
  rintro X ⟨F, hF⟩
  exact ⟨.limit F hF⟩

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