mulIndicator_const_eq_mulIndicator_const

English

If a ∈ s is equivalent to b ∈ t, then s.mulIndicator c at a equals t.mulIndicator c at b for any c.

Русский

Если a принадлежит s тогда и только тогда, когда b принадлежит t, то s.mulIndicator c в a равен t.mulIndicator c в b для любого c.

LaTeX

$$$s.\text{mulIndicator} (\lambda _ . c)\ a = t.\text{mulIndicator} (\lambda _ . c)\ b$ при условии $a \in s \iff b \in t$$$

Lean4

@[to_additive]
theorem mulIndicator_const_eq_mulIndicator_const {t : Set β} {b : β} {c : M} (h : a ∈ s ↔ b ∈ t) :
    s.mulIndicator (fun _ ↦ c) a = t.mulIndicator (fun _ ↦ c) b :=
  mulIndicator_eq_mulIndicator h rfl

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