Theorem Filter.HasBasis.iInter_mul_left_eq_closure

Modification history

2026-08-19 02:29
Mathlib/Topology/Algebra/Group/Pointwise.lean
feat(Topology/Semicontinuity/Michael): michael's selection theorem (#39116) …
Added Filter.HasBasis.iInter_mul_left_eq_closureView on Github →