left — Mathlib

English

A binary injective function is injective when only the left argument varies.

Русский

Двоичную инъективную функцию инъективна, когда варьируется только первый аргумент.

LaTeX

$$$ \\forall {f : \\alpha \\to \\beta \\to \\gamma}, \\operatorname{Injective2} f \\to \\forall (b : \\beta), \\operatorname{Injective} (\\lambda a, f a b) $$$

Lean4

/-- A binary injective function is injective when only the left argument varies. -/
protected theorem left (hf : Injective2 f) (b : β) : Function.Injective fun a ↦ f a b := fun _ _ h ↦ (hf h).left

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