English
The product indicator of unions interacts with germ-indicators: the germ of a union equals the product of the germ indicators for the components, in appropriate settings.
Русский
Индикатор произведения для объединений взаимодействует с индикаторами герма: germ( s ∪ t ) = germ(s) · germ(t) в подходящих условиях.
LaTeX
$$$ (s \\cup t).mulIndicator f = (s.mulIndicator f) * (t.mulIndicator f)$ in Germ sense$$
Lean4
@[to_additive]
theorem mulIndicator_eventuallyEq (hf : f =ᶠ[l ⊓ 𝓟 s] g) (hs : s =ᶠ[l] t) : mulIndicator s f =ᶠ[l] mulIndicator t g :=
(eventually_inf_principal.1 hf).mp <|
hs.mem_iff.mono fun x hst hfg =>
by_cases (fun hxs : x ∈ s => by simp only [*, hst.1 hxs, mulIndicator_of_mem])
(fun hxs => by simp only [mulIndicator_of_notMem, hxs, mt hst.2 hxs, not_false_eq_true])
