Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-11 21:30 8c1b484d

View on Github →

feat(topology/sets/compacts): add positive_compacts.map (#18872) Also adds some missing functorial lemmas about map.

Estimated changes

Modified src/topology/sets/compacts.lean

modified theorem topological_space.compact_opens.coe_map

added theorem topological_space.compact_opens.map_comp

added theorem topological_space.compact_opens.map_id

added theorem topological_space.compacts.coe_equiv_apply_eq_preimage

modified theorem topological_space.compacts.coe_map

added theorem topological_space.compacts.equiv_refl

added theorem topological_space.compacts.equiv_symm

deleted theorem topological_space.compacts.equiv_to_fun_val

added theorem topological_space.compacts.equiv_trans

added theorem topological_space.compacts.map_comp

added theorem topological_space.compacts.map_id

added theorem topological_space.positive_compacts.coe_map

added theorem topological_space.positive_compacts.map_comp

added theorem topological_space.positive_compacts.map_id