hasCardinalLT_arrow_shrinkHoms_iff

English

HasCardinalLT (Arrow (ShrinkHoms C)) κ is equivalent to HasCardinalLT (Arrow C) κ.

Русский

HasCardinalLT (Arrow (ShrinkHoms C)) κ эквивалентно HasCardinalLT (Arrow C) κ.

LaTeX

$$$\\\\operatorname{HasCardinalLT}(\\\\operatorname{Arrow}(\\\\operatorname{ShrinkHoms}(C)),\\\\kappa) \\\\iff \\\\operatorname{HasCardinalLT}(\\\\operatorname{Arrow}(C),\\\\kappa)$$$

Lean4

@[simp]
theorem hasCardinalLT_arrow_shrinkHoms_iff (C : Type u) [Category.{v} C] [LocallySmall.{w'} C] (κ : Cardinal.{w}) :
    HasCardinalLT (Arrow.{w'} (ShrinkHoms C)) κ ↔ HasCardinalLT (Arrow C) κ :=
  hasCardinalLT_iff_of_equiv (Arrow.shrinkHomsEquiv C) κ

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