Commit 2024-01-25 09:21 9a290c22

View on Github →

chore(Topology/Constructions): rename most type variables (#9863) Now we use letters X and Y for topological spaces, not Greek letters. I didn't replace all letters; some lemmas need a large number of different letters. Volunteers for the last instances welcome.

Estimated changes

modified theorem CofiniteTopology.isOpen_iff
modified theorem CofiniteTopology.nhds_eq
modified def CofiniteTopology.of
modified def CofiniteTopology
modified theorem Continuous.Prod.mk
modified theorem Continuous.Prod.mk_left
modified theorem Continuous.codRestrict
modified theorem Continuous.comp₂
modified theorem Continuous.comp₃
modified theorem Continuous.comp₄
modified theorem Continuous.fst'
modified theorem Continuous.fst
modified theorem Continuous.prod_map
modified theorem Continuous.prod_mk
modified theorem Continuous.quotient_lift
modified theorem Continuous.quotient_liftOn'
modified theorem Continuous.quotient_map'
modified theorem Continuous.restrict
modified theorem Continuous.restrictPreimage
modified theorem Continuous.snd'
modified theorem Continuous.snd
modified theorem Continuous.subtype_map
modified theorem Continuous.subtype_mk
modified theorem Continuous.subtype_val
modified theorem Continuous.sum_elim
modified theorem Continuous.sum_map
modified theorem Continuous.update
modified theorem ContinuousAt.fst''
modified theorem ContinuousAt.fst'
modified theorem ContinuousAt.fst
modified theorem ContinuousAt.prod
modified theorem ContinuousAt.prod_map'
modified theorem ContinuousAt.prod_map
modified theorem ContinuousAt.restrict
modified theorem ContinuousAt.snd''
modified theorem ContinuousAt.snd'
modified theorem ContinuousAt.snd
modified theorem ContinuousAt.update
modified theorem Dense.prod
modified theorem Dense.quotient
modified theorem DenseRange.prod_map
modified theorem DenseRange.quotient
modified theorem Embedding.codRestrict
modified theorem Embedding.prod_map
modified theorem Filter.Eventually.prod_nhds
modified theorem Filter.HasBasis.prod_nhds'
modified theorem Filter.HasBasis.prod_nhds
modified theorem Filter.Tendsto.apply
modified theorem Filter.Tendsto.prod_mk_nhds
modified theorem Filter.Tendsto.update
modified theorem Inducing.codRestrict
modified theorem Inducing.of_codRestrict
modified theorem Inducing.prod_map
modified theorem IsClosed.prod
modified theorem IsClosed.setOf_mapsTo
modified theorem IsClosed.trans
modified theorem IsOpen.prod
modified theorem IsOpen.trans
modified theorem IsOpenMap.restrict
modified theorem IsOpenMap.sum_elim
modified theorem Pi.continuous_postcomp'
modified theorem Pi.continuous_postcomp
modified theorem Pi.induced_precomp
modified theorem Prod.tendsto_iff
modified theorem Quotient.preimage_mem_nhds
modified theorem Subtype.dense_iff
modified theorem ULift.closedEmbedding_down
modified theorem ULift.isClosed_iff
modified theorem ULift.isOpen_iff
modified theorem closedEmbedding_inl
modified theorem closedEmbedding_inr
modified theorem closure_prod_eq
modified theorem continuousAt_fst
modified theorem continuousAt_pi
modified theorem continuousAt_snd
modified theorem continuousAt_subtype_val
modified theorem continuous_curry
modified theorem continuous_fst
modified theorem continuous_inclusion
modified theorem continuous_inf_dom_left₂
modified theorem continuous_inf_dom_right₂
modified theorem continuous_inl
modified theorem continuous_inr
modified theorem continuous_isLeft
modified theorem continuous_isRight
modified theorem continuous_ofAdd
modified theorem continuous_ofDual
modified theorem continuous_ofMul
modified theorem continuous_prod_mk
modified theorem continuous_quot_lift
modified theorem continuous_quot_mk
modified theorem continuous_quotient_mk'
modified theorem continuous_sInf_dom₂
modified theorem continuous_sigma
modified theorem continuous_sigma_iff
modified theorem continuous_snd
modified theorem continuous_subtype_val
modified theorem continuous_sum_dom
modified theorem continuous_sum_elim
modified theorem continuous_sum_map
modified theorem continuous_swap
modified theorem continuous_toAdd
modified theorem continuous_toDual
modified theorem continuous_toMul
modified theorem continuous_uLift_down
modified theorem continuous_uLift_up
modified theorem continuous_uncurry_left
modified theorem continuous_uncurry_right
modified theorem embedding_graph
modified theorem embedding_inclusion
modified theorem embedding_inl
modified theorem embedding_inr
modified theorem embedding_prod_mk
modified theorem embedding_subtype_val
modified theorem embedding_uLift_down
modified theorem exists_nhds_square
modified theorem frontier_prod_eq
modified theorem frontier_prod_univ_eq
modified theorem frontier_univ_prod_eq
modified theorem inducing_const_prod
modified theorem inducing_prod_const
modified theorem inducing_sigma
modified theorem inducing_subtype_val
modified theorem interior_prod_eq
modified theorem isClosedMap_ofAdd
modified theorem isClosedMap_ofDual
modified theorem isClosedMap_ofMul
modified theorem isClosedMap_swap
modified theorem isClosedMap_toAdd
modified theorem isClosedMap_toDual
modified theorem isClosedMap_toMul
modified theorem isClosed_range_inl
modified theorem isClosed_range_inr
modified theorem isClosed_sum_iff
modified theorem isOpenMap_fst
modified theorem isOpenMap_inl
modified theorem isOpenMap_inr
modified theorem isOpenMap_ofAdd
modified theorem isOpenMap_ofDual
modified theorem isOpenMap_ofMul
modified theorem isOpenMap_sigma
modified theorem isOpenMap_snd
modified theorem isOpenMap_sum
modified theorem isOpenMap_sum_elim
modified theorem isOpenMap_toAdd
modified theorem isOpenMap_toDual
modified theorem isOpenMap_toMul
modified theorem isOpen_prod_iff'
modified theorem isOpen_prod_iff
modified theorem isOpen_range_inl
modified theorem isOpen_range_inr
modified theorem isOpen_sum_iff
modified theorem map_fst_nhds
modified theorem map_fst_nhdsWithin
modified theorem map_mem_closure₂
modified theorem map_nhds_subtype_val
modified theorem map_snd_nhds
modified theorem map_snd_nhdsWithin
modified theorem mem_nhdsWithin_prod_iff
modified theorem mem_nhds_prod_iff'
modified theorem mem_nhds_prod_iff
modified theorem mem_nhds_subtype
modified theorem nhdsWithin_prod_eq
modified theorem nhds_inl
modified theorem nhds_inr
modified theorem nhds_ne_subtype_eq_bot_iff
modified theorem nhds_ne_subtype_neBot_iff
modified theorem nhds_ofAdd
modified theorem nhds_ofDual
modified theorem nhds_ofMul
modified theorem nhds_prod_eq
modified theorem nhds_subtype
modified theorem nhds_subtype_eq_comap
modified theorem nhds_swap
modified theorem nhds_toAdd
modified theorem nhds_toDual
modified theorem nhds_toMul
modified theorem openEmbedding_inl
modified theorem openEmbedding_inr
modified theorem prod_induced_induced
modified theorem prod_mem_nhds
modified theorem prod_mem_nhds_iff
modified theorem quotientMap_quot_mk
modified theorem quotientMap_quotient_mk'
modified theorem tendsto_pi_nhds
modified theorem tendsto_subtype_rng