Theorem Trivialization.open_target'

Modification history

2024-06-28 09:13

Mathlib/Topology/FiberBundle/Trivialization.lean

chore(*): remove some deprecated theorems (#14214)

Deleted Trivialization.open_target'View on Github →

2023-03-10 06:58

Mathlib/Topology/FiberBundle/Trivialization.lean

feat: port Topology.FiberBundle.Trivialization (#2707)

Added Trivialization.open_target'View on Github →