English
The map Pi.map f is injective if and only if each coordinate map f(i) is injective.
Русский
Пусть Pi.map f инъективен тогда и только тогда, когда каждая карта f(i) инъективна.
LaTeX
$$$\operatorname{Injective}(\Pi\text{-map}\ f) \iff \forall i, \operatorname{Injective}(f(i))$$$
Lean4
@[simp]
theorem _root_.Pi.map_injective {ι : Sort*} {α β : ι → Sort*} [∀ i, Nonempty (α i)] {f : ∀ i, α i → β i} :
Injective (Pi.map f) ↔ ∀ i, Injective (f i)
where
mp h i x y
hxy := by
classical
have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
replace h := @h (Function.update default i x) (Function.update default i y) ?_
· simpa using congrFun h i
rw [Pi.map_update, Pi.map_update, hxy]
mpr := .piMap
