curry_inj — Mathlib

English

If curry c1 n1 equals curry c2 n2, then c1 = c2 and n1 = n2.

Русский

Если curry c1 n1 = curry c2 n2, то c1 = c2 и n1 = n2.

LaTeX

$$$\\forall {c_1\\ c_2\\ n_1\\ n_2},\\ (\\mathrm{curry}\\ c_1\\ n_1 = \\mathrm{curry}\\ c_2\\ n_2) \\Rightarrow (c_1 = c_2) \\wedge (n_1 = n_2)$$$

Lean4

theorem curry_inj {c₁ c₂ n₁ n₂} (h : curry c₁ n₁ = curry c₂ n₂) : c₁ = c₂ ∧ n₁ = n₂ :=
  ⟨by injection h, by
    injection h with h₁ h₂
    injection h₂ with h₃ h₄
    exact const_inj h₃⟩

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