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_iInter_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
· simp_all
· rw [mulIndicator_of_notMem hx]
simp only [mem_iInter, not_forall] at hx
rcases hx with ⟨j, hj⟩
refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_
simpa [mulIndicator_of_notMem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x
