hasCardinalLT_option_iff — Mathlib

English

For X and κ with aleph0 ≤ κ, HasCardinalLT (Option X) κ is equivalent to HasCardinalLT X κ.

Русский

Для X и κ с алф0 ≤ κ, HasCardinalLT (Option X) κ эквивалентно HasCardinalLT X κ.

LaTeX

$$HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ$$

Lean4

theorem hasCardinalLT_option_iff (X : Type u) (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ :=
  by
  rw [hasCardinalLT_iff_of_equiv (Equiv.optionEquivSumPUnit.{0} X), hasCardinalLT_sum_iff _ _ _ hκ,
    and_iff_left_iff_imp]
  refine fun _ ↦ HasCardinalLT.of_le ?_ hκ
  rw [hasCardinalLT_aleph0_iff]
  infer_instance

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