mapDomain_congr — Mathlib

English

If two maps f and g agree on the support of a finsupp x, then mapDomain f x = mapDomain g x.

Русский

Если две функции f и g совпадают на опоре x, то сопоставления одинаковы.

LaTeX

$$$(\\forall x \\in v.{\\text{support}}\\, f x = g x) \\Rightarrow v.mapDomain f = v.mapDomain g$$$

Lean4

theorem mapDomain_congr {f g : α → β} (h : ∀ x ∈ v.support, f x = g x) : v.mapDomain f = v.mapDomain g :=
  Finset.sum_congr rfl fun _ H => by simp only [h _ H]

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