add_le_aleph0 — Mathlib

English

For any cardinals c1, c2, c1 + c2 ≤ ℵ₀ iff c1 ≤ ℵ₀ and c2 ≤ ℵ₀.

Русский

Для любых кардиналов c1, c2, c1 + c2 ≤ ℵ₀ тогда и только тогда, когда c1 ≤ ℵ₀ и c2 ≤ ℵ₀.

LaTeX

$$$ c_1 + c_2 \le \aleph_0 \iff c_1 \le \aleph_0 \land c_2 \le \aleph_0$$$

Lean4

@[simp]
theorem add_le_aleph0 {c₁ c₂ : Cardinal} : c₁ + c₂ ≤ ℵ₀ ↔ c₁ ≤ ℵ₀ ∧ c₂ ≤ ℵ₀ :=
  ⟨fun h => ⟨le_self_add.trans h, le_add_self.trans h⟩, fun h => aleph0_add_aleph0 ▸ add_le_add h.1 h.2⟩

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