aleph0_le_mul_iff — Mathlib

English

ℵ0 ≤ a · b if and only if a ≠ 0, b ≠ 0 and (ℵ0 ≤ a or ℵ0 ≤ b).

Русский

ℵ0 ≤ a · b тогда и только тогда a ≠ 0, b ≠ 0 и (ℵ0 ≤ a или ℵ0 ≤ b).

LaTeX

$$$ \aleph_0 \le a \cdot b \iff a \neq 0 \wedge b \neq 0 \wedge (\aleph_0 \le a \lor \aleph_0 \le b)$$$

Lean4

/-- See also `Cardinal.aleph0_le_mul_iff`. -/
theorem aleph0_le_mul_iff {a b : Cardinal} : ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b) :=
  by
  let h := (@mul_lt_aleph0_iff a b).not
  rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h

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