Mathlib Changelog
v3
Changelog
About
Github
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