English
Assuming bottom equals 1 in M, for a family of sets s i, and f, x, we have mulIndicator (⋃ i, s i) f x = ⨆ i, mulIndicator (s i) f x.
Русский
При условии, что нижний элемент равен единице, для семейства множеств s_i и функции f имеем mulIndicator(⋃ i, s_i) f x = ⨆ i, mulIndicator(s_i) f x.
LaTeX
$$(⊥ : M) = 1 → mulIndicator (⋃ i, s i) f x = ⨆ i, mulIndicator (s i) f x$$
Lean4
@[to_additive]
theorem mulIndicator_iUnion_apply (h1 : (⊥ : M) = 1) (s : ι → Set α) (f : α → M) (x : α) :
mulIndicator (⋃ i, s i) f x = ⨆ i, mulIndicator (s i) f x :=
by
by_cases hx : x ∈ ⋃ i, s i
· rw [mulIndicator_of_mem hx]
rw [mem_iUnion] at hx
refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
rcases hx with ⟨i, hi⟩
exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)
· rw [mulIndicator_of_notMem hx]
simp only [mem_iUnion, not_exists] at hx
simp [hx, ← h1]
