mulIndicator_congr — Mathlib

English

If two functions f and g agree on a set s (EqOn f g s), then the indicator of s applied to f equals the indicator of s applied to g; i.e., mulIndicator s f = mulIndicator s g.

Русский

Если f и g согласуются на множестве s (EqOn f g s), то индикаторы на s дают одинаковые значения: mulIndicator s f = mulIndicator s g.

LaTeX

$$$$\\text{EqOn}(f,g,s) \\;\Longrightarrow\\; s.mulIndicator\, f = s.mulIndicator\, g.$$$$

Lean4

@[to_additive]
theorem mulIndicator_congr (h : EqOn f g s) : mulIndicator s f = mulIndicator s g :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs with h_1
    · exact h h_1
    rfl

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