Theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symmL_apply_of_notMem

Modification history

2026-06-23 10:53
Mathlib/Topology/VectorBundle/Basic.lean
feat(Topology): generalise `Trivialization.symm` (#40903) …
Added Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symmL_apply_of_notMemView on Github →