Commit 2023-05-22 12:09 2f771251

View on Github →

chore: forward-port leanprover-community/mathlib#18872 (#3958)

Estimated changes

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.CompactOpens.map_comp

added theorem TopologicalSpace.CompactOpens.map_id

added theorem TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage

added theorem TopologicalSpace.Compacts.equiv_refl

added theorem TopologicalSpace.Compacts.equiv_symm

deleted theorem TopologicalSpace.Compacts.equiv_to_fun_val

added theorem TopologicalSpace.Compacts.equiv_trans

added theorem TopologicalSpace.Compacts.map_comp

added theorem TopologicalSpace.Compacts.map_id

added theorem TopologicalSpace.PositiveCompacts.coe_map

added theorem TopologicalSpace.PositiveCompacts.map_comp

added theorem TopologicalSpace.PositiveCompacts.map_id