mulIndicator_one — Mathlib

English

Let l be a filter on a set X and f : X → β, where β has a multiplicative identity 1. If f is eventually equal to 1 with respect to l, then for every subset s ⊆ X, the function x ↦ (s.mulIndicator f)(x) is also eventually equal to 1 along l.

Русский

Пусть l — фильтр на множестве X, и f: X → β, где β имеет единицу умножения 1. Если f эквивалентна 1 по фильтру l на бесконечно большем множестве, то для любого подмножества s ⊆ X функция x ↦ (s.mulIndicator f)(x) тоже эквивалентна 1 по l.

LaTeX

$$$ f =^f_l 1 \\Rightarrow s\\mathrm{mulIndicator}(f) =^f_l 1 $$$

Lean4

@[to_additive]
theorem mulIndicator_one [One β] {l : Filter α} {f : α → β} {s : Set α} (hf : f =ᶠ[l] 1) : s.mulIndicator f =ᶠ[l] 1 :=
  hf.mulIndicator.trans <| by rw [mulIndicator_one']

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