Commit 2024-03-05 15:28 fbca142e

View on Github →

refactor(CompactOpen): redefine in terms of Set.image2 and Set.MapsTo (#11053)

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

deleted def ContinuousMap.CompactOpen.gen

modified def ContinuousMap.coev

added theorem ContinuousMap.compactOpen_eq_iInf_induced

deleted theorem ContinuousMap.compactOpen_eq_mapsTo

deleted theorem ContinuousMap.compactOpen_eq_sInf_induced

modified theorem ContinuousMap.continuous_coev

modified theorem ContinuousMap.continuous_curry'

modified def ContinuousMap.curry'

modified def ContinuousMap.curry

modified theorem ContinuousMap.curry_apply

deleted theorem ContinuousMap.gen_empty

deleted theorem ContinuousMap.gen_empty_right

deleted theorem ContinuousMap.gen_inter

deleted theorem ContinuousMap.gen_union

deleted theorem ContinuousMap.gen_univ

modified theorem ContinuousMap.image_coev

modified theorem ContinuousMap.isOpen_setOf_mapsTo

added theorem ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced

deleted theorem ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced