ext_iff_mulSupport — Mathlib

English

Two functions f and g are equal iff they have the same mulSupport and agree on that mulSupport.

Русский

Две функции равны тогда и только тогда, когда имеют одну и ту же mulSupport и согласованы на ней.

LaTeX

$$$ f = g \\iff \\mathrm{mulSupport}(f) = \\mathrm{mulSupport}(g) \\land \\forall x \\in \\mathrm{mulSupport}(f), f(x) = g(x) $$$

Lean4

@[to_additive]
theorem ext_iff_mulSupport : f = g ↔ f.mulSupport = g.mulSupport ∧ ∀ x ∈ f.mulSupport, f x = g x
    where
  mp h := h ▸ ⟨rfl, fun _ _ ↦ rfl⟩
  mpr := fun ⟨h₁, h₂⟩ ↦
    funext fun x ↦ by
      if hx : x ∈ f.mulSupport then exact h₂ x hx
      else rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

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