Commit 2023-01-31 20:49 fb5f6b71

View on Github →

feat: port Topology.Constructions (#1906)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Constructions.lean

added theorem CofiniteTopology.isClosed_iff

added theorem CofiniteTopology.isOpen_iff'

added theorem CofiniteTopology.isOpen_iff

added theorem CofiniteTopology.mem_nhds_iff

added theorem CofiniteTopology.nhds_eq

added def CofiniteTopology.of

added def CofiniteTopology

added theorem Continuous.Prod.mk

added theorem Continuous.Prod.mk_left

added theorem Continuous.codRestrict

added theorem Continuous.comp₂

added theorem Continuous.comp₃

added theorem Continuous.comp₄

added theorem Continuous.fin_insertNth

added theorem Continuous.fst'

added theorem Continuous.fst

added theorem Continuous.prod_map

added theorem Continuous.prod_mk

added theorem Continuous.quotient_lift

added theorem Continuous.quotient_liftOn'

added theorem Continuous.quotient_map'

added theorem Continuous.sigma_map

added theorem Continuous.snd'

added theorem Continuous.snd

added theorem Continuous.subtype_map

added theorem Continuous.subtype_mk

added theorem Continuous.subtype_val

added theorem Continuous.sum_elim

added theorem Continuous.sum_map

added theorem Continuous.update

added theorem ContinuousAt.fin_insertNth

added theorem ContinuousAt.fst''

added theorem ContinuousAt.fst'

added theorem ContinuousAt.fst

added theorem ContinuousAt.prod

added theorem ContinuousAt.prod_map'

added theorem ContinuousAt.prod_map

added theorem ContinuousAt.restrict

added theorem ContinuousAt.restrictPreimage

added theorem ContinuousAt.snd''

added theorem ContinuousAt.snd'

added theorem ContinuousAt.snd

added theorem ContinuousAt.update

added theorem Dense.prod

added theorem Dense.quotient

added theorem DenseRange.prod_map

added theorem DenseRange.quotient

added theorem DiscreteTopology.of_subset

added theorem Embedding.codRestrict

added theorem Embedding.prod_map

added theorem Filter.Eventually.curry_nhds

added theorem Filter.Eventually.prod_inl_nhds

added theorem Filter.Eventually.prod_inr_nhds

added theorem Filter.Eventually.prod_mk_nhds

added theorem Filter.Eventually.prod_nhds

added theorem Filter.HasBasis.prod_nhds'

added theorem Filter.HasBasis.prod_nhds

added theorem Filter.Tendsto.apply

added theorem Filter.Tendsto.fin_insertNth

added theorem Filter.Tendsto.prod_mk_nhds

added theorem Filter.Tendsto.update

added theorem Inducing.codRestrict

added theorem Inducing.of_codRestrict

added theorem Inducing.prod_map

added theorem IsClosed.prod

added theorem IsOpen.isOpenMap_subtype_val

added theorem IsOpen.openEmbedding_subtype_val

added theorem IsOpen.prod

added theorem IsOpenMap.restrict

added theorem IsOpenMap.sum_elim

added theorem Prod.tendsto_iff

added theorem Quotient.preimage_mem_nhds

added theorem Sigma.nhds_eq

added theorem Sigma.nhds_mk

added theorem Subtype.dense_iff

added theorem closedEmbedding_inl

added theorem closedEmbedding_inr

added theorem closedEmbedding_sigmaMk

added theorem closedEmbedding_subtype_val

added theorem closure_prod_eq

added theorem closure_subtype

added theorem comap_sigmaMk_nhds

added theorem continuousAt_apply

added theorem continuousAt_codRestrict_iff

added theorem continuousAt_fst

added theorem continuousAt_pi

added theorem continuousAt_snd

added theorem continuousAt_subtype_val

added theorem continuous_apply

added theorem continuous_apply_apply

added theorem continuous_curry

added theorem continuous_fst

added theorem continuous_inclusion

added theorem continuous_inf_dom_left₂

added theorem continuous_inf_dom_right₂

added theorem continuous_infₛ_dom₂

added theorem continuous_inl

added theorem continuous_inr

added theorem continuous_ofAdd

added theorem continuous_ofDual

added theorem continuous_ofMul

added theorem continuous_pi

added theorem continuous_pi_iff

added theorem continuous_prod_mk

added theorem continuous_quot_lift

added theorem continuous_quot_mk

added theorem continuous_quotient_mk'

added theorem continuous_sigma

added theorem continuous_sigmaMk

added theorem continuous_sigma_iff

added theorem continuous_sigma_map

added theorem continuous_snd

added theorem continuous_subtype_nhds_cover

added theorem continuous_subtype_val

added theorem continuous_sum_elim

added theorem continuous_sum_map

added theorem continuous_swap

added theorem continuous_toAdd

added theorem continuous_toDual

added theorem continuous_toMul

added theorem continuous_uLift_down

added theorem continuous_uLift_up

added theorem continuous_uncurry_left

added theorem continuous_uncurry_of_discreteTopology

added theorem continuous_uncurry_of_discreteTopology_left

added theorem continuous_uncurry_right

added theorem continuous_update

added theorem discreteTopology_subtype_iff

added theorem embedding_graph

added theorem embedding_inclusion

added theorem embedding_inl

added theorem embedding_inr

added theorem embedding_sigmaMk

added theorem embedding_sigma_map

added theorem embedding_subtype_val

added theorem embedding_uLift_down

added theorem exists_finset_piecewise_mem_of_mem_nhds

added theorem exists_nhds_square

added theorem frontier_prod_eq

added theorem frontier_prod_univ_eq

added theorem frontier_univ_prod_eq

added theorem inducing_infᵢ_to_pi

added theorem inducing_sigma_map

added theorem inducing_subtype_val

added theorem interior_pi_set

added theorem interior_prod_eq

added theorem isClosedMap_ofAdd

added theorem isClosedMap_ofDual

added theorem isClosedMap_ofMul

added theorem isClosedMap_sigmaMk

added theorem isClosedMap_toAdd

added theorem isClosedMap_toDual

added theorem isClosedMap_toMul

added theorem isClosed_range_inl

added theorem isClosed_range_inr

added theorem isClosed_range_sigmaMk

added theorem isClosed_set_pi

added theorem isClosed_sigma_iff

added theorem isClosed_sum_iff

added theorem isOpenMap_fst

added theorem isOpenMap_inl

added theorem isOpenMap_inr

added theorem isOpenMap_ofAdd

added theorem isOpenMap_ofDual

added theorem isOpenMap_ofMul

added theorem isOpenMap_sigma

added theorem isOpenMap_sigmaMk

added theorem isOpenMap_sigma_map

added theorem isOpenMap_snd

added theorem isOpenMap_sum

added theorem isOpenMap_sum_elim

added theorem isOpenMap_toAdd

added theorem isOpenMap_toDual

added theorem isOpenMap_toMul

added theorem isOpen_prod_iff'

added theorem isOpen_prod_iff

added theorem isOpen_range_inl

added theorem isOpen_range_inr

added theorem isOpen_range_sigmaMk

added theorem isOpen_set_pi

added theorem isOpen_sigma_fst_preimage

added theorem isOpen_sigma_iff

added theorem isOpen_sum_iff

added theorem map_fst_nhds

added theorem map_fst_nhdsWithin

added theorem map_mem_closure₂

added theorem map_nhds_subtype_coe_eq

added theorem map_snd_nhds

added theorem map_snd_nhdsWithin

added theorem mem_nhds_of_pi_mem_nhds

added theorem mem_nhds_prod_iff'

added theorem mem_nhds_prod_iff

added theorem mem_nhds_subtype

added theorem nhdsWithin_prod_eq

added theorem nhdsWithin_subtype_eq_bot_iff

added theorem nhds_inl

added theorem nhds_inr

added theorem nhds_ne_subtype_eq_bot_iff

added theorem nhds_ne_subtype_neBot_iff

added theorem nhds_ofAdd

added theorem nhds_ofDual

added theorem nhds_ofMul

added theorem nhds_pi

added theorem nhds_prod_eq

added theorem nhds_subtype

added theorem nhds_subtype_eq_comap

added theorem nhds_swap

added theorem nhds_toAdd

added theorem nhds_toDual

added theorem nhds_toMul

added theorem openEmbedding_inl

added theorem openEmbedding_inr

added theorem openEmbedding_sigmaMk

added theorem openEmbedding_sigma_map

added theorem pi_eq_generateFrom

added theorem pi_generateFrom_eq

added theorem pi_generateFrom_eq_finite

added theorem prod_eq_generateFrom

added theorem prod_generateFrom_generateFrom_eq

added theorem prod_induced_induced

added theorem prod_mem_nhds

added theorem prod_mem_nhds_iff

added theorem quotientMap_quot_mk

added theorem quotientMap_quotient_mk'

added theorem set_pi_mem_nhds

added theorem set_pi_mem_nhds_iff

added theorem tendsto_pi_nhds

added theorem tendsto_subtype_rng