English
Let l be a filter on α, f : α → β with One β. If f(x) ≠ 1 for l-almost all x and s.mulIndicator f =ᶠ[l] t.mulIndicator f, then s =ᶠ[l] t.
Русский
Пусть l — фильтр на α, f: α → β с единицей 1. Если f(x) ≠ 1 для множества большинства x по l и s.mulIndicator f эквивалентно t.mulIndicator f по l, то s эквивалентно t по l.
LaTeX
$$$\\bigl(\\forall^\infty x\\in l,\, f(x) \\ne 1\\bigr) \\Rightarrow \\bigl(s\\mulIndicator f =^f_l t\\mulIndicator f\\bigr) \\Rightarrow s =^f_l t$$$
Lean4
@[to_additive]
theorem of_mulIndicator [One β] {l : Filter α} {f : α → β} (hf : ∀ᶠ x in l, f x ≠ 1) {s t : Set α}
(h : s.mulIndicator f =ᶠ[l] t.mulIndicator f) : s =ᶠ[l] t :=
by
have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦
by
rw [mulSupport_mulIndicator]
exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
exact this.symm.trans <| h.mulSupport.trans this
