mulIndicator_eq_mulIndicator — Mathlib

English

Suppose t is a set and there is a correspondence h1: a ∈ s ↔ b ∈ t between a and b, and h2: f a = g b. Then the indicator values match: s.mulIndicator f a = t.mulIndicator g b.

Русский

Пусть существует соответствие между точками a и b через h1: a ∈ s ↔ b ∈ t и h2: f a = g b. Тогда значения индикаторов совпадают: s.mulIndicator f a = t.mulIndicator g b.

LaTeX

$$$$(h1: a \in s \leftrightarrow b \in t) \Rightarrow (h2: f\,a = g\,b) \Rightarrow s.mulIndicator f a = t.mulIndicator g b.$$$$

Lean4

@[to_additive]
theorem mulIndicator_eq_mulIndicator {t : Set β} {g : β → M} {b : β} (h1 : a ∈ s ↔ b ∈ t) (h2 : f a = g b) :
    s.mulIndicator f a = t.mulIndicator g b := by by_cases a ∈ s <;> simp_all

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