Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-10 16:41 2ac1f20a

View on Github →

rename open -> is_open, closed -> is_closed

Estimated changes

Modified topology/continuity.lean

deleted theorem closed_diagonal

deleted theorem closed_eq

deleted theorem closed_prod

deleted theorem closed_property2

deleted theorem closed_property3

deleted theorem closed_property

modified def continuous

modified theorem continuous_Prop

deleted theorem continuous_iff_closed

added theorem continuous_iff_is_closed

deleted theorem continuous_subtype_closed_cover

added theorem continuous_subtype_is_closed_cover

deleted theorem embedding_closed

added theorem embedding_is_closed

added theorem is_closed_diagonal

added theorem is_closed_eq

added theorem is_closed_prod

added theorem is_closed_property2

added theorem is_closed_property3

added theorem is_closed_property

added theorem is_open_induced

added theorem is_open_set_prod

added theorem is_open_singleton_true

deleted theorem open_induced

deleted theorem open_set_prod

deleted theorem open_singleton_true

Modified topology/real.lean

deleted theorem closed_ge

deleted theorem closed_imp

deleted theorem closed_le

deleted theorem closed_le_real

added theorem is_closed_ge

added theorem is_closed_imp

added theorem is_closed_le

added theorem is_closed_le_real

added theorem is_open_gt

added theorem is_open_lt

added theorem is_open_lt_real

deleted theorem open_gt

deleted theorem open_lt

deleted theorem open_lt_real

Modified topology/topological_space.lean

deleted def closed

deleted theorem closed_Inter

deleted theorem closed_Union

deleted theorem closed_Union_of_locally_finite

deleted theorem closed_closure

deleted theorem closed_compl_iff

deleted theorem closed_empty

deleted theorem closed_iff_nhds

deleted theorem closed_induced_iff

deleted theorem closed_inter

deleted theorem closed_sInter

deleted theorem closed_singleton

deleted theorem closed_union

deleted theorem closed_univ

modified def closure

deleted theorem closure_eq_iff_closed

added theorem closure_eq_iff_is_closed

deleted theorem closure_eq_of_closed

added theorem closure_eq_of_is_closed

modified theorem closure_inter_open

modified theorem closure_minimal

deleted theorem closure_subset_iff_subset_of_closed

added theorem closure_subset_iff_subset_of_is_closed

deleted theorem compact_of_closed_subset

added theorem compact_of_is_closed_subset

modified theorem generate_from_le

modified def interior

modified theorem interior_eq_iff_open

modified theorem interior_eq_of_open

modified theorem interior_maximal

deleted theorem interior_union_closed_of_interior_empty

added theorem interior_union_is_closed_of_interior_empty

added def is_closed

added theorem is_closed_Inter

added theorem is_closed_Union

added theorem is_closed_Union_of_locally_finite

added theorem is_closed_closure

added theorem is_closed_compl_iff

added theorem is_closed_empty

added theorem is_closed_iff_nhds

added theorem is_closed_induced_iff

added theorem is_closed_inter

added theorem is_closed_sInter

added theorem is_closed_singleton

added theorem is_closed_union

added theorem is_closed_univ

added def is_open

added theorem is_open_Union

added theorem is_open_compl_iff

added theorem is_open_diff

added theorem is_open_empty

added theorem is_open_iff_nhds

added theorem is_open_inter

added theorem is_open_interior

added theorem is_open_sUnion

added theorem is_open_union

added theorem is_open_univ

modified theorem mem_nhds_sets

modified def nhds

deleted theorem nhds_closed

added theorem nhds_is_closed

modified theorem nhds_sets

deleted def open'

deleted theorem open_Union

deleted theorem open_compl_iff

deleted theorem open_diff

deleted theorem open_empty

deleted theorem open_iff_nhds

deleted theorem open_inter

deleted theorem open_interior

deleted theorem open_sUnion

deleted theorem open_union

deleted theorem open_univ

modified theorem subset_interior_iff_subset_of_open

modified theorem topological_space_eq

modified theorem towards_nhds

Modified topology/uniform_space.lean

deleted theorem compact_of_totally_bounded_closed

added theorem compact_of_totally_bounded_is_closed

deleted theorem complete_of_closed

added theorem complete_of_is_closed

added theorem is_open_uniformity

deleted theorem mem_uniformity_closed

added theorem mem_uniformity_is_closed

deleted theorem open_uniformity