Commit 2023-12-30 06:21 3286beab

View on Github →

chore(Topology/CompactOpen): rename type variables (#9328) Use X, Y, Z instead of α, β, γ for topological spaces.

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

modified def ContinuousMap.CompactOpen.gen

modified theorem ContinuousMap.coe_const'

modified def ContinuousMap.coev

modified theorem ContinuousMap.compactOpen_eq

modified theorem ContinuousMap.compactOpen_le_induced

modified def ContinuousMap.const'

modified theorem ContinuousMap.continuous.comp'

modified theorem ContinuousMap.continuous_coe

modified theorem ContinuousMap.continuous_coev

modified theorem ContinuousMap.continuous_comp'

modified theorem ContinuousMap.continuous_comp

modified theorem ContinuousMap.continuous_comp_left

modified theorem ContinuousMap.continuous_compactOpen

modified theorem ContinuousMap.continuous_const'

modified theorem ContinuousMap.continuous_curry'

modified theorem ContinuousMap.continuous_curry

modified theorem ContinuousMap.continuous_eval

modified theorem ContinuousMap.continuous_eval_const

modified theorem ContinuousMap.continuous_of_continuous_uncurry

modified theorem ContinuousMap.continuous_restrict

modified theorem ContinuousMap.continuous_uncurry

modified theorem ContinuousMap.continuous_uncurry_of_continuous

modified def ContinuousMap.curry'

modified def ContinuousMap.curry

modified theorem ContinuousMap.curry_apply

modified theorem ContinuousMap.embedding_comp

modified theorem ContinuousMap.eventually_mapsTo

modified theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall

modified theorem ContinuousMap.gen_empty

modified theorem ContinuousMap.gen_empty_right

modified theorem ContinuousMap.gen_inter

modified theorem ContinuousMap.gen_union

modified theorem ContinuousMap.gen_univ

modified theorem ContinuousMap.image_coev

modified theorem ContinuousMap.inducing_comp

modified theorem ContinuousMap.isClopen_setOf_mapsTo

modified theorem ContinuousMap.isClosed_setOf_mapsTo

modified theorem ContinuousMap.isOpen_setOf_mapsTo

modified theorem ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced

modified theorem ContinuousMap.tendsto_compactOpen_iff_forall

modified theorem ContinuousMap.tendsto_compactOpen_restrict

modified theorem ContinuousMap.tendsto_nhds_compactOpen

modified def ContinuousMap.uncurry

modified def Homeomorph.continuousMapOfUnique

modified theorem Homeomorph.continuousMapOfUnique_apply

modified theorem Homeomorph.continuousMapOfUnique_symm_apply

modified def Homeomorph.curry