mul_lt_aleph0_iff_of_ne_zero — Mathlib

English

Let a and b be cardinals with a ≠ 0 and b ≠ 0. Then a · b < ℵ₀ if and only if a < ℵ₀ and b < ℵ₀.

Русский

Пусть a и b — кардиналы и оба не равны нулю. Тогда a · b < ℵ₀ тогда и только тогда, когда a < ℵ₀ и b < ℵ₀.

LaTeX

$$$ \forall a,b\ (a \neq 0 \land b \neq 0)\; \bigl(a \cdot b < \aleph_0 \iff a < \aleph_0 \land b < \aleph_0\bigr)$$$

Lean4

theorem mul_lt_aleph0_iff_of_ne_zero {a b : Cardinal} (ha : a ≠ 0) (hb : b ≠ 0) : a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀ := by
  simp [mul_lt_aleph0_iff, ha, hb]

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