Def FiberPrebundle.trivializationOfMemPretrivializationAtlas

Modification history

2023-03-22 01:31

Mathlib/Topology/FiberBundle/Basic.lean

feat: port Topology.FiberBundle.Basic (#2862)

Added FiberPrebundle.trivializationOfMemPretrivializationAtlas View on Github →