mulIndicator_union_of_disjoint — Mathlib

English

If s and t are disjoint, then mulIndicator (s ∪ t) f equals the function a ↦ mulIndicator s f a · mulIndicator t f a.

Русский

Если s и t несовпадающие, то mulIndicator (s ∪ t) f = a ↦ mulIndicator s f a · mulIndicator t f a.

LaTeX

$$$\\mathrm{mulIndicator}(s \\cup t) f = (a \\mapsto \\mathrm{mulIndicator}(s) f a \\cdot \\mathrm{mulIndicator}(t) f a)$.$$

Lean4

@[to_additive]
theorem mulIndicator_union_of_disjoint (h : Disjoint s t) (f : α → M) :
    mulIndicator (s ∪ t) f = fun a => mulIndicator s f a * mulIndicator t f a :=
  funext fun _ => mulIndicator_union_of_notMem_inter (fun ha => h.le_bot ha) _

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