Theorem ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff

Modification history

2026-04-01 16:05
Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces (#35661)
Added ChartedSpace.liftPropWithinAt_subtypeVal_comp_iffView on Github →