Theorem FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp

Modification history

2023-05-29 23:41
Mathlib/Topology/FiberBundle/Basic.lean
feat: forward-port 19107 (#4470) …
Added FiberPrebundle.inducing_totalSpaceMk_of_inducing_compView on Github →