hasCardinalLT_arrow_shrink_iff — Mathlib

English

HasCardinalLT (Arrow (Shrink C)) κ ↔ HasCardinalLT (Arrow C) κ.

Русский

HasCardinalLT (Arrow (Shrink C)) κ ⇔ HasCardinalLT (Arrow C) κ.

LaTeX

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

Lean4

@[simp]
theorem hasCardinalLT_arrow_shrink_iff (C : Type u) [Category.{v} C] [Small.{w'} C] (κ : Cardinal.{w}) :
    HasCardinalLT (Arrow (Shrink.{w'} C)) κ ↔ HasCardinalLT (Arrow C) κ :=
  hasCardinalLT_iff_of_equiv (Arrow.shrinkEquiv C) κ

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