Commit 2023-03-22 13:29 7a3acfc6

View on Github →

feat: port Topology.Covering (#3031)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Covering.lean

added theorem IsCoveringMap.mk

added def IsCoveringMap

added theorem IsCoveringMapOn.mk

added def IsCoveringMapOn

added theorem IsEvenlyCovered.mem_toTrivialization_baseSet

added theorem IsEvenlyCovered.toTrivialization_apply

added theorem IsEvenlyCovered.to_isEvenlyCovered_preimage

added def IsEvenlyCovered

added theorem isCoveringMap_iff_isCoveringMapOn_univ