hasCardinalLT_iff_of_equiv — Mathlib

English

HasCardinalLT X κ holds if and only if HasCardinalLT Y κ holds for any equivalence e: X ≃ Y.

Русский

HasCardinalLT X κ выполняется тогда и только тогда, когда HasCardinalLT Y κ выполняется для эквивалентности e: X ≃ Y.

LaTeX

$$HasCardinalLT X κ ↔ HasCardinalLT Y κ$$

Lean4

theorem hasCardinalLT_iff_of_equiv {X : Type u} {Y : Type u'} (e : X ≃ Y) (κ : Cardinal.{v}) :
    HasCardinalLT X κ ↔ HasCardinalLT Y κ :=
  ⟨fun h ↦ h.of_injective _ e.symm.injective, fun h ↦ h.of_injective _ e.injective⟩

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