Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 10:23 d8510cac

View on Github →

feat(topology/local_at_target): Properties of continuous maps that are local at the target. (#15452)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.range_subtype_map

Modified src/data/set/function.lean

added theorem set.maps_to.coe_restrict

added theorem set.maps_to.range_restrict

added theorem set.range_restrict_preimage

added def set.restrict_preimage

Modified src/data/set/lattice.lean

added theorem set.bijective_iff_bijective_of_Union_eq_univ

added theorem set.injective_iff_injective_of_Union_eq_univ

added theorem set.restrict_preimage_bijective

added theorem set.restrict_preimage_injective

added theorem set.restrict_preimage_surjective

added theorem set.surjective_iff_surjective_of_Union_eq_univ

Modified src/topology/constructions.lean

added theorem continuous_at.restrict

added theorem continuous_at.restrict_preimage

added theorem continuous_at_cod_restrict_iff

Modified src/topology/continuous_function/basic.lean

added def continuous_map.restrict_preimage

Created src/topology/local_at_target.lean

added theorem closed_embedding_iff_closed_embedding_of_supr_eq_top

added theorem closed_iff_coe_preimage_of_supr_eq_top

added theorem embedding_iff_embedding_of_supr_eq_top

added theorem inducing_iff_inducing_of_supr_eq_top

added theorem open_embedding_iff_open_embedding_of_supr_eq_top

added theorem open_iff_coe_preimage_of_supr_eq_top

added theorem open_iff_inter_of_supr_eq_top

added theorem set.restrict_preimage_closed_embedding

added theorem set.restrict_preimage_embedding

added theorem set.restrict_preimage_inducing

added theorem set.restrict_preimage_open_embedding

Modified src/topology/maps.lean

added theorem inducing.is_closed_preimage