Theorems · Theorem · general topology

indicator_eventuallyEq

∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s t : Set α} {f g : α → M} {l : Filter α},
  f =ᶠ[l ⊓ Filter.principal s] g → s =ᶠ[l] t → s.indicator f =ᶠ[l] t.indicator g

Defined in

Mathlib.Order.Filter.IndicatorFunction

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Zero