uncurry — Mathlib

English

If a two-argument function f is injective in both arguments (Injective2 f), then the uncurried function uncurry f: α × β → γ is injective.

Русский

Если функция f: α → β → γ инъективна по обоим аргументам (Injective2 f), то раскрытая функция uncurry f: α × β → γ инъективна.

LaTeX

$$$ \forall {\alpha \beta \gamma} {f : \alpha \to \beta \to \gamma},\; \operatorname{Injective2} f \Rightarrow \operatorname{Injective} (\operatorname{uncurry} f)$$$

Lean4

protected theorem uncurry {α β γ : Type*} {f : α → β → γ} (hf : Injective2 f) : Function.Injective (uncurry f) :=
  fun ⟨_, _⟩ ⟨_, _⟩ h ↦ (hf h).elim (congr_arg₂ _)

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