Theorem LowerHemicontinuous.hasOpenCGraph_of_add_hasOpenCGraph

Modification history

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