Commit 2023-02-11 09:23 a908df61

View on Github →

feat: port Topology.CompactOpen (#2123)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/CompactOpen.lean

added def ContinuousMap.CompactOpen.gen

added theorem ContinuousMap.coe_const'

added def ContinuousMap.coev

added theorem ContinuousMap.compactOpen_eq_infₛ_induced

added theorem ContinuousMap.compactOpen_le_induced

added def ContinuousMap.const'

added theorem ContinuousMap.continuous.comp'

added theorem ContinuousMap.continuous_coe'

added theorem ContinuousMap.continuous_coev

added theorem ContinuousMap.continuous_comp'

added theorem ContinuousMap.continuous_comp

added theorem ContinuousMap.continuous_comp_left

added theorem ContinuousMap.continuous_const'

added theorem ContinuousMap.continuous_curry'

added theorem ContinuousMap.continuous_curry

added theorem ContinuousMap.continuous_eval'

added theorem ContinuousMap.continuous_eval_const'

added theorem ContinuousMap.continuous_of_continuous_uncurry

added theorem ContinuousMap.continuous_restrict

added theorem ContinuousMap.continuous_uncurry

added theorem ContinuousMap.continuous_uncurry_of_continuous

added def ContinuousMap.curry'

added def ContinuousMap.curry

added theorem ContinuousMap.curry_apply

added theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall

added theorem ContinuousMap.gen_empty

added theorem ContinuousMap.gen_empty_right

added theorem ContinuousMap.gen_inter

added theorem ContinuousMap.gen_union

added theorem ContinuousMap.gen_univ

added theorem ContinuousMap.image_coev

added theorem ContinuousMap.nhds_compactOpen_eq_infₛ_nhds_induced

added theorem ContinuousMap.tendsto_compactOpen_iff_forall

added theorem ContinuousMap.tendsto_compactOpen_restrict

added def ContinuousMap.uncurry

added def Homeomorph.continuousMapOfUnique

added theorem Homeomorph.continuousMapOfUnique_apply

added theorem Homeomorph.continuousMapOfUnique_symm_apply

added def Homeomorph.curry

added theorem QuotientMap.continuous_lift_prod_left

added theorem QuotientMap.continuous_lift_prod_right