English
If f: α → β → γ is injective in both arguments and α is nonempty, then the map b ↦ f a b is injective for every fixed a, i.e., the function (λ b a ↦ f a b) is injective.
Русский
Если f: α → β → γ инъективна по обоим аргументам и α непусто, то для каждого фиксированного a отображение b ↦ f a b инъективно.
LaTeX
$$$ \forall {\alpha \beta \gamma} {f : \alpha \to \beta \to \gamma},\; \operatorname{Injective2} f \Rightarrow [\operatorname{Nonempty} \alpha] \Rightarrow \operatorname{Injective} (\lambda b a \mapsto f a b)$$$
Lean4
/-- As a map from the right argument to a unary function, `f` is injective. -/
theorem right' (hf : Injective2 f) [Nonempty α] : Function.Injective fun b a ↦ f a b := fun _ _ h ↦
let ⟨a⟩ := ‹Nonempty α›
hf.right a <| (congr_fun h a :)
