right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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