mapDomain_apply — Mathlib

English

If a value a is not in the range of f, then the corresponding coordinate of mapDomain f x is zero.

Русский

Если значение a не лежит в образе f, то соответствующая координата mapDomain f x равна нулю.

LaTeX

$$$a \\notin \\operatorname{range}(f) \\Rightarrow (\\operatorname{mapDomain} f\\, x)\\, a = 0.$$$

Lean4

theorem mapDomain_apply {f : α → β} (hf : Function.Injective f) (x : α →₀ M) (a : α) : mapDomain f x (f a) = x a :=
  by
  rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]
  · intro b _ hba
    exact single_eq_of_ne' (hf.ne hba)
  · intro _
    rw [single_zero, coe_zero, Pi.zero_apply]

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