AB4StarOfSize_shrink — Mathlib

English

Shrinking the size preserves AB4StarOfSize via hasProducts_shrink.

Русский

Уменьшение размера сохраняет AB4StarOfSize через hasProducts_shrink.

LaTeX

$$$[HasProducts.{w} C] \land [AB4StarOfSize.{w} C] \Rightarrow AB4StarOfSize.{0} C$$$

Lean4

theorem AB4StarOfSize_shrink [HasProducts.{max w w'} C] [AB4StarOfSize.{max w w'} C] :
    haveI : HasProducts.{w} C := hasProducts_shrink.{w, w'}
    AB4StarOfSize.{w} C :=
  haveI := hasProducts_shrink.{w, w'} (C := C)
  ⟨fun J ↦
    HasExactLimitsOfShape.of_domain_equivalence C (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩

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