Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-03 19:05 201413b9

View on Github →

chore(topology): Splits topology.basic and topology.continuity (#785) Also, the most basic aspects of continuity are now in topology.basic

Estimated changes

deleted theorem closure_singleton
deleted theorem coinduced_compose
deleted theorem coinduced_id
deleted theorem coinduced_inf
deleted theorem coinduced_infi
deleted theorem coinduced_mono
deleted theorem coinduced_top
deleted def compact
deleted theorem compact_Union_of_compact
deleted theorem compact_adherence_nhdset
deleted theorem compact_bUnion_of_compact
deleted theorem compact_diff
deleted theorem compact_empty
deleted theorem compact_inter
deleted theorem compact_of_closed
deleted theorem compact_of_finite
deleted theorem compact_singleton
deleted theorem compact_union_of_compact
deleted theorem compact_univ
deleted theorem compl_singleton_mem_nhds
deleted def connected_component
added theorem continuous.comp
added theorem continuous.tendsto
added def continuous
added def continuous_at
added theorem continuous_const
added theorem continuous_id
added theorem continuous_if
added def continuous_on
deleted theorem eq_irreducible_component
deleted theorem eq_of_nhds_eq_nhds
deleted theorem eq_of_nhds_neq_bot
deleted theorem eq_top_of_singletons_open
deleted theorem exists_irreducible
deleted theorem exists_mem_inter
deleted theorem gc_induced_coinduced
deleted theorem gc_nhds
deleted theorem generate_from_le
deleted theorem generate_from_mono
deleted def gi_generate_from
deleted theorem induced_bot
deleted theorem induced_compose
deleted theorem induced_generate_from_eq
deleted theorem induced_id
deleted theorem induced_mono
deleted theorem induced_sup
deleted theorem induced_supr
deleted def is_clopen
deleted theorem is_clopen_compl
deleted theorem is_clopen_compl_iff
deleted theorem is_clopen_diff
deleted theorem is_clopen_empty
deleted theorem is_clopen_iff
deleted theorem is_clopen_inter
deleted theorem is_clopen_union
deleted theorem is_clopen_univ
deleted theorem is_closed_induced_iff
deleted theorem is_closed_singleton
deleted def is_connected
deleted theorem is_connected_closure
deleted theorem is_connected_empty
deleted theorem is_connected_sUnion
deleted theorem is_connected_singleton
deleted theorem is_connected_union
deleted def is_irreducible
deleted theorem is_irreducible_closure
deleted theorem is_irreducible_empty
deleted theorem is_irreducible_singleton
deleted theorem is_open_coinduced
deleted theorem is_open_discrete
deleted theorem is_open_induced_iff
deleted theorem le_of_nhds_le_nhds
deleted theorem lim_eq
deleted theorem lim_nhds_eq
deleted theorem lim_nhds_eq_of_closure
added theorem mem_closure
deleted theorem mem_connected_component
deleted theorem mem_irreducible_component
deleted theorem mem_nhds_induced
deleted theorem mem_nhds_subtype
deleted theorem mem_nhds_within_subtype
deleted theorem mk_of_closure_sets
deleted theorem nhds_Sup
deleted theorem nhds_bot
deleted theorem nhds_cons
deleted theorem nhds_discrete
deleted theorem nhds_eq_nhds_iff
deleted theorem nhds_induced
deleted theorem nhds_is_closed
deleted theorem nhds_le_nhds_iff
deleted theorem nhds_list
deleted theorem nhds_mono
deleted theorem nhds_nil
deleted theorem nhds_subtype
deleted theorem nhds_sup
deleted theorem nhds_supr
deleted theorem nhds_top
deleted theorem nhds_within_subtype
deleted theorem normal_separation
added def pcontinuous
added theorem pcontinuous_iff'
deleted theorem principal_subtype
deleted theorem quotient_dense_of_dense
deleted theorem t2_iff_nhds
deleted theorem t2_iff_ultrafilter
deleted theorem t2_separation
deleted theorem tendsto_nhds_unique
deleted theorem closure_induced
deleted theorem compact_image
deleted theorem compact_range
deleted theorem continuous.comp
deleted theorem continuous.tendsto
deleted def continuous
deleted theorem continuous_Inf_dom
deleted theorem continuous_Inf_rng
deleted theorem continuous_Prop
deleted theorem continuous_Sup_dom
deleted theorem continuous_Sup_rng
deleted def continuous_at
deleted theorem continuous_at_within_univ
deleted theorem continuous_bot
deleted theorem continuous_coinduced_dom
deleted theorem continuous_coinduced_rng
deleted theorem continuous_const
deleted theorem continuous_generated_from
deleted theorem continuous_id
deleted theorem continuous_if
deleted theorem continuous_iff_induced_le
deleted theorem continuous_iff_is_closed
deleted theorem continuous_induced_dom
deleted theorem continuous_induced_rng
deleted theorem continuous_inf_dom
deleted theorem continuous_inf_rng_left
deleted theorem continuous_inf_rng_right
deleted theorem continuous_infi_dom
deleted theorem continuous_infi_rng
deleted theorem continuous_le_dom
deleted theorem continuous_le_rng
deleted def continuous_on
deleted theorem continuous_on_iff'
deleted theorem continuous_on_iff
deleted theorem continuous_sup_dom_left
deleted theorem continuous_sup_dom_right
deleted theorem continuous_sup_rng
deleted theorem continuous_supr_dom
deleted theorem continuous_supr_rng
deleted theorem continuous_top
deleted theorem dense_embedding.extend_eq
deleted theorem dense_embedding.inj_iff
deleted theorem dense_embedding.mk'
deleted structure dense_embedding
deleted theorem embedding.continuous
deleted theorem embedding.continuous_iff
deleted theorem embedding.map_nhds_eq
deleted def embedding
deleted theorem embedding_compose
deleted theorem embedding_id
deleted theorem embedding_is_closed
deleted theorem embedding_open
deleted theorem embedding_prod_mk
deleted theorem is_open_induced
deleted theorem is_open_induced_eq
deleted theorem is_open_map.of_inverse
deleted def is_open_map
deleted theorem is_open_map_iff_nhds_le
deleted theorem is_open_singleton_true
deleted theorem map_nhds_induced_eq
deleted theorem mem_closure
deleted theorem nhds_induced_eq_comap
deleted theorem nhds_within_le_comap
deleted theorem open_dom_of_pcontinuous
deleted def pcontinuous
deleted theorem pcontinuous_iff'
deleted def quotient_map
added theorem continuous_Prop
added theorem dense_embedding.mk'
added structure dense_embedding
added theorem embedding.continuous
added theorem embedding.map_nhds_eq
added def embedding
added theorem embedding_compose
added theorem embedding_id
added theorem embedding_is_closed
added theorem embedding_open
added theorem embedding_prod_mk
added theorem is_open_map.of_inverse
added def is_open_map
added theorem is_open_singleton_true
added def quotient_map
added theorem closure_induced
added theorem coinduced_compose
added theorem coinduced_id
added theorem coinduced_inf
added theorem coinduced_infi
added theorem coinduced_mono
added theorem coinduced_top
added theorem continuous_Inf_dom
added theorem continuous_Inf_rng
added theorem continuous_Sup_dom
added theorem continuous_Sup_rng
added theorem continuous_bot
added theorem continuous_induced_dom
added theorem continuous_induced_rng
added theorem continuous_inf_dom
added theorem continuous_infi_dom
added theorem continuous_infi_rng
added theorem continuous_le_dom
added theorem continuous_le_rng
added theorem continuous_on_iff'
added theorem continuous_on_iff
added theorem continuous_sup_rng
added theorem continuous_supr_dom
added theorem continuous_supr_rng
added theorem continuous_top
added theorem eq_of_nhds_eq_nhds
added theorem gc_induced_coinduced
added theorem gc_nhds
added theorem generate_from_le
added theorem generate_from_mono
added def gi_generate_from
added theorem induced_bot
added theorem induced_compose
added theorem induced_id
added theorem induced_mono
added theorem induced_sup
added theorem induced_supr
added theorem is_closed_induced_iff
added theorem is_open_coinduced
added theorem is_open_discrete
added theorem is_open_induced
added theorem is_open_induced_eq
added theorem is_open_induced_iff
added theorem le_of_nhds_le_nhds
added theorem map_nhds_induced_eq
added theorem mem_nhds_induced
added theorem mem_nhds_subtype
added theorem mk_of_closure_sets
added theorem nhds_Sup
added theorem nhds_bot
added theorem nhds_cons
added theorem nhds_discrete
added theorem nhds_induced
added theorem nhds_induced_eq_comap
added theorem nhds_list
added theorem nhds_mono
added theorem nhds_nil
added theorem nhds_subtype
added theorem nhds_sup
added theorem nhds_supr
added theorem nhds_top
added theorem nhds_within_le_comap
added theorem nhds_within_subtype
added theorem principal_subtype
added theorem closure_singleton
added theorem eq_of_nhds_neq_bot
added theorem is_closed_singleton
added theorem lim_eq
added theorem lim_nhds_eq
added theorem lim_nhds_eq_of_closure
added theorem nhds_eq_nhds_iff
added theorem nhds_is_closed
added theorem nhds_le_nhds_iff
added theorem normal_separation
added theorem t2_iff_nhds
added theorem t2_iff_ultrafilter
added theorem t2_separation
added theorem tendsto_nhds_unique
added def compact
added theorem compact_diff
added theorem compact_empty
added theorem compact_image
added theorem compact_inter
added theorem compact_of_closed
added theorem compact_of_finite
added theorem compact_range
added theorem compact_singleton
added theorem compact_univ
added theorem exists_irreducible
added theorem exists_mem_inter
added def is_clopen
added theorem is_clopen_compl
added theorem is_clopen_compl_iff
added theorem is_clopen_diff
added theorem is_clopen_empty
added theorem is_clopen_iff
added theorem is_clopen_inter
added theorem is_clopen_union
added theorem is_clopen_univ
added def is_connected
added theorem is_connected_closure
added theorem is_connected_empty
added theorem is_connected_sUnion
added theorem is_connected_singleton
added theorem is_connected_union
added def is_irreducible
added theorem is_irreducible_closure
added theorem is_irreducible_empty