of_mulIndicator_const — Mathlib

English

Let l be a filter on α and c ∈ β with c ≠ 1. If s.mulIndicator (fun _ ↦ c) =ᶠ[l] t.mulIndicator (fun _ ↦ c), then s =ᶠ[l] t.

Русский

Пусть l — фильтр на α и c ∈ β с c ≠ 1. Если константный индикатор по s равен константному индикатору по t почти как по l, то множества s и t равны по l.

LaTeX

$$$ c \\ne 1 \\Rightarrow \\bigl(s.mulIndicator (\\lambda _ . c) =^f_l t.mulIndicator (\\lambda _ . c)\\bigr) \\Rightarrow s =^f_l t $$$

Lean4

@[to_additive]
theorem of_mulIndicator_const [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s t : Set α}
    (h : s.mulIndicator (fun _ ↦ c) =ᶠ[l] t.mulIndicator fun _ ↦ c) : s =ᶠ[l] t :=
  .of_mulIndicator (Eventually.of_forall fun _ ↦ hc) h

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