const_inj — Mathlib

English

The function const : Nat → Code is injective; if const(n1) = const(n2) then n1 = n2.

Русский

Функция const : Nat → Code инъективна; если const(n1) = const(n2), то n1 = n2.

LaTeX

$$$\\forall n_1,n_2 \\; (\\mathrm{const}(n_1) = \\mathrm{const}(n_2) \\Rightarrow n_1 = n_2)$$$

Lean4

theorem const_inj : ∀ {n₁ n₂}, Nat.Partrec.Code.const n₁ = Nat.Partrec.Code.const n₂ → n₁ = n₂
  | 0, 0, _ => by simp
  | n₁ + 1, n₂ + 1, h => by
    dsimp [Nat.Partrec.Code.const] at h
    injection h with h₁ h₂
    simp only [const_inj h₂]

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