Theorem Filter.EventuallyEmptyOrUniv.mulIndicator_const_iff

Modification history

2026-09-03 20:16
Mathlib/Order/Filter/EventuallyConst.lean
refactor: definition for `EventuallyConst` on `Set` (#43114) …
Added Filter.EventuallyEmptyOrUniv.mulIndicator_const_iffView on Github →