add_eq_two_iff — Mathlib

English

For n,m ∈ WithBot ℕ, n + m = 2 iff (n = 0 ∧ m = 2) ∨ (n = 1 ∧ m = 1) ∨ (n = 2 ∧ m = 0).

Русский

Для n,m ∈ WithBot ℕ, n + m = 2 тогда и только тогда, когда (n = 0 ∧ m = 2) или (n = 1 ∧ m = 1) или (n = 2 ∧ m = 0).

LaTeX

$$$$ n + m = 2 \\\\iff (n = 0 \\\\land m = 2) \\\\lor (n = 1 \\\\land m = 1) \\\\lor (n = 2 \\\\land m = 0) $$$$

Lean4

theorem add_eq_two_iff {n m : WithBot ℕ} : n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 :=
  by
  cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_two_iff]

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