add_eq_one_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 :=
  by
  cases n
  · simp only [WithBot.bot_add, WithBot.bot_ne_one, WithBot.bot_ne_zero, false_and, or_self]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_one_iff]

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