support_congr — Mathlib

English

If f.support ⊆ g.support and f(x)=g(x) for all x in g.support, then f=g.

Русский

Если support(f) ⊆ support(g) и f(x)=g(x) для всех x в support(g), то f=g.

LaTeX

$$$$ f.support \subseteq g.support \quad\text{and}\quad \forall x\in g.support,\ f(x)=g(x) \;\Rightarrow\; f=g. $$$$

Lean4

theorem support_congr (h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g :=
  by
  ext x
  by_cases hx : x ∈ g.support
  · exact h' x hx
  · rw [notMem_support.mp hx, ← notMem_support]
    exact fun H => hx (h H)

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