nsmul_lt_aleph0_iff — Mathlib

English

For any n and a, n times a is below aleph0 iff n = 0 or a < aleph0.

Русский

Для любого n и a: n · a < aleph0 тогда и только тогда n = 0 или a < aleph0.

LaTeX

$$$ n \cdot a < \aleph_0 \iff n = 0 \lor a < \aleph_0 $$$

Lean4

/-- See also `Cardinal.nsmul_lt_aleph0_iff_of_ne_zero` if you already have `n ≠ 0`. -/
theorem nsmul_lt_aleph0_iff {n : ℕ} {a : Cardinal} : n • a < ℵ₀ ↔ n = 0 ∨ a < ℵ₀ := by
  cases n with
  | zero => simpa using nat_lt_aleph0 0
  | succ n =>
    simp only [Nat.succ_ne_zero, false_or]
    induction n with
    | zero => simp
    | succ n ih => rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]

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