aleph0_le_mul_iff' — Mathlib

English

Variant formulation: a · b ≥ ℵ0 is equivalent to certain nonzero and countable conditions; see standard equivalences.

Русский

Вариант формулировки: a · b ≥ ℵ0 эквивалентно определённым ненулевым и счётным условиям; см. стандартные эквивалентности.

LaTeX

$$$ \aleph_0 \le a \cdot b \iff \text{(complex condition as in standard form)} $$$

Lean4

/-- See also `Cardinal.aleph0_le_mul_iff'`. -/
theorem aleph0_le_mul_iff' {a b : Cardinal.{u}} : ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0 :=
  by
  have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a
  simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]
  simp only [and_comm, or_comm]

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