hasCardinalLT_of_hasCardinalLT_arrow

English

If HasCardinalLT (Arrow C) κ holds, then HasCardinalLT C κ also holds.

Русский

Если HasCardinalLT (Arrow C) κ, то HasCardinalLT C κ.

LaTeX

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

Lean4

theorem hasCardinalLT_of_hasCardinalLT_arrow {C : Type u} [Category.{v} C] {κ : Cardinal.{w}}
    (h : HasCardinalLT (Arrow C) κ) : HasCardinalLT C κ :=
  h.of_injective (fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)

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