Theorem HasOpenLowerSections.exists_continuous_selection

Modification history

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