map_eq_iff — Mathlib

English

Two direct-sum elements have the same image under map f iff all coordinate images agree after applying f_i.

Русский

Изображения двух элементов прямой суммы одинаковы под map f тогда и только тогда, когда после применения f_i совпадают соответствующие координаты.

LaTeX

$$$$\\mathrm{map}\; f\\; x = \\mathrm{map}\\; f\\; y \\iff \\forall i,\\ f_i(x_i) = f_i(y_i).$$$$

Lean4

theorem map_eq_iff (x y : ⨁ i, α i) : map f x = map f y ↔ ∀ i, f i (x i) = f i (y i) := by
  simp_rw [DirectSum.ext_iff, map_apply]

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