English
For κ ≥ aleph0, HasCardinalLT (X ⊕ Y) κ is equivalent to HasCardinalLT X κ and HasCardinalLT Y κ.
Русский
При κ ≥ aleph0 выполнено: HasCardinalLT (X ⊕ Y) κ эквивалентно HasCardinalLT X κ и HasCardinalLT Y κ.
LaTeX
$$HasCardinalLT (X \\oplus Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ$$
Lean4
theorem hasCardinalLT_sum_iff (X : Type u) (Y : Type u') (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) :
HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ :=
by
constructor
· intro h
exact ⟨h.of_injective _ Sum.inl_injective, h.of_injective _ Sum.inr_injective⟩
· rintro ⟨hX, hY⟩
dsimp [HasCardinalLT] at hX hY ⊢
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at hX
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift] at hY
simp only [Cardinal.mk_sum, Cardinal.lift_add, Cardinal.lift_lift]
exact Cardinal.add_lt_of_lt (by simpa using hκ) hX hY
