Theorem MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm

Modification history

2023-06-27 14:29
Mathlib/Geometry/Manifold/Complex.lean
feat: port Geometry.Manifold.Complex (#5498)
Added MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_normView on Github →