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