add_le_add_iff_of_lt_aleph0 — Mathlib

English

For γ < aleph0, α + γ ≤ β + γ iff α ≤ β.

Русский

Для γ < ℵ0 верно: α + γ ≤ β + γ ⇔ α ≤ β.

LaTeX

$$$\gamma < \aleph_0 \Rightarrow (\alpha + \gamma \le \beta + \gamma) \iff (\alpha \le \beta)$$$

Lean4

theorem add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < ℵ₀) : α + γ ≤ β + γ ↔ α ≤ β :=
  by
  refine ⟨fun h => ?_, fun h => add_le_add_right h γ⟩
  contrapose h
  rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
  exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩

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