AB4OfSize_shrink — Mathlib

English

Under univLE and size-shrink hypotheses, AB4OfSize propagates from a larger size to a smaller one.

Русский

При наличии ограничений Универсального уровня и уменьшения объёма, свойство AB4OfSize переносится с большего размера на меньший.

LaTeX

$$$\mathrm{AB4OfSize}(w,w')(C) \Leftarrow \mathrm{HasFilteredColimitsOfSize}(w_2,w_2')(C) \wedge \mathrm{UnivLE}(w,w_2) \wedge \mathrm{UnivLE}(w',w_2')$$$

Lean4

theorem AB4OfSize_shrink [HasCoproducts.{max w w'} C] [AB4OfSize.{max w w'} C] :
    haveI : HasCoproducts.{w} C := hasCoproducts_shrink.{w, w'}
    AB4OfSize.{w} C :=
  haveI := hasCoproducts_shrink.{w, w'} (C := C)
  ⟨fun J ↦
    HasExactColimitsOfShape.of_domain_equivalence C (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩

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