Theorem IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset

Modification history

2025-07-21 14:23
Mathlib/Topology/Order/IntermediateValue.lean
feat: define Riemannian manifolds (#27250) …
Added IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subsetView on Github →