hasCardinalLT_arrow_walkingParallelFamily

English

If T is a type with cardinal LT κ and κ ≥ aleph0, then the arrow category of WalkingParallelFamily T has cardinal LT κ.

Русский

Если T — тип с кардиналом LT κ и κ не меньше aleph0, то стрелочное множество WalkingParallelFamily T имеет Cardinal LT κ.

LaTeX

$$$HasCardinalLT(Arrow(WalkingParallelFamily\ T))\kappa$$$

Lean4

theorem hasCardinalLT_arrow_walkingParallelFamily {T : Type u} {κ : Cardinal.{w}} (hT : HasCardinalLT T κ)
    (hκ : Cardinal.aleph0 ≤ κ) : HasCardinalLT (Arrow (WalkingParallelFamily T)) κ := by
  simpa only [hasCardinalLT_iff_of_equiv (WalkingParallelFamily.arrowEquiv T), hasCardinalLT_option_iff _ _ hκ] using hT

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