nsmul_lt_aleph0_iff_of_ne_zero — Mathlib

English

If n ≠ 0, then n · a < aleph0 iff a < aleph0.

Русский

Если n ≠ 0, тогда n · a < aleph0 тогда и только тогда a < aleph0.

LaTeX

$$$ n \neq 0 \Rightarrow (n \cdot a < \aleph_0 \iff a < \aleph_0) $$$

Lean4

/-- See also `Cardinal.nsmul_lt_aleph0_iff` for a hypothesis-free version. -/
theorem nsmul_lt_aleph0_iff_of_ne_zero {n : ℕ} {a : Cardinal} (h : n ≠ 0) : n • a < ℵ₀ ↔ a < ℵ₀ :=
  nsmul_lt_aleph0_iff.trans <| or_iff_right h

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