add_eq_three_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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