mulIndicator_const_eventuallyEq — Mathlib

English

For a filter l and c ≠ 1, the statement that the constant-indicator on s and t are eventually equal is equivalent to s and t being eventually equal.

Русский

Пусть для фильтра l и c ≠ 1 индикатор константы на s и на t эквивалентны почти по l, тогда множества s и t эквивалентны по l.

LaTeX

$$$\\text{Ne}(c,1) \\Rightarrow (s.mulIndicator (\\lambda x. c) =^f_l t.mulIndicator (\\lambda x. c) \\iff s =^f_l t)$$$

Lean4

@[to_additive]
theorem mulIndicator_const_eventuallyEq [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s t : Set α} :
    s.mulIndicator (fun _ ↦ c) =ᶠ[l] t.mulIndicator (fun _ ↦ c) ↔ s =ᶠ[l] t :=
  ⟨.of_mulIndicator_const hc, mulIndicator_eventuallyEq .rfl⟩

Похожие утверждения