Theorem closure_subset_mul_left_of_mem_nhds_one

Modification history

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