mulIndicator_union_of_notMem_inter

English

If a ∉ s ∩ t, then mulIndicator (s ∪ t) f a = mulIndicator s f a · mulIndicator t f a.

Русский

Если a ∉ s ∩ t, то mulIndicator (s ∪ t) f a = mulIndicator s f a · mulIndicator t f a.

LaTeX

$$$\\text{If } a \\notin s \\cap t, \\quad \\mathrm{mulIndicator}(s \\cup t) f a = \\mathrm{mulIndicator}(s) f a \\cdot \\mathrm{mulIndicator}(t) f a.$$$

Lean4

@[to_additive]
theorem mulIndicator_union_of_notMem_inter (h : a ∉ s ∩ t) (f : α → M) :
    mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a := by
  rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, mul_one]

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