lmap_eq_iff — Mathlib

English

Equality of lmap f x and lmap f y is equivalent to coordinatewise equality f_i(x_i) = f_i(y_i) for all i.

Русский

Равенство lmap f x и lmap f y эквивалентно равенству по координатам f_i(x_i) = f_i(y_i) для всех i.

LaTeX

$$$lmap\\ f\\ x = lmap\\ f\\ y \\iff \\forall i,\\ f_i(x_i) = f_i(y_i).$$$

Lean4

theorem lmap_eq_iff (x y : ⨁ i, M i) : lmap f x = lmap f y ↔ ∀ i, f i (x i) = f i (y i) :=
  map_eq_iff (fun i => (f i).toAddMonoidHom) _ _

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