English
Let h1: ⊥ = 1, f monotone, s monotone. Then ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i).
Русский
Пусть h1: ⊥ = 1, f монотонна, s монотонна; тогда ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i).
LaTeX
$$$h1 \land hf \land hs \Rightarrow \bigvee_i (s_i).mulIndicator(f_i) = (\bigcup_i s_i).mulIndicator( \bigvee_i f_i )$$$
Lean4
@[to_additive]
theorem iSup_mulIndicator {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f : ι → α → M} {s : ι → Set α}
(h1 : (⊥ : M) = 1) (hf : Monotone f) (hs : Monotone s) :
⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i) :=
by
simp only [le_antisymm_iff, iSup_le_iff]
refine
⟨fun i ↦
(mulIndicator_mono (le_iSup _ _)).trans
(mulIndicator_le_mulIndicator_of_subset (subset_iUnion _ _) (fun _ ↦ by simp [← h1])),
fun a ↦ ?_⟩
by_cases ha : a ∈ ⋃ i, s i
· obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]
refine iSup_le fun j ↦ ?_
obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_
rw [mulIndicator_of_mem (hs hik hi)]
· rw [mulIndicator_of_notMem ha, ← h1]
exact bot_le
