Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 10:35 a348944f

View on Github →

chore(topology): rename compact to is_compact (#3356)

Estimated changes

deleted theorem compact.Inf_mem
deleted theorem compact.Sup_mem
deleted theorem compact.bdd_above
deleted theorem compact.bdd_below
deleted theorem compact.exists_forall_ge
deleted theorem compact.exists_forall_le
deleted theorem compact.exists_is_glb
deleted theorem compact.exists_is_least
deleted theorem compact.exists_is_lub
deleted theorem compact.is_glb_Inf
deleted theorem compact.is_greatest_Sup
deleted theorem compact.is_least_Inf
deleted theorem compact.is_lub_Sup
modified theorem eq_Icc_of_connected_compact
added theorem is_compact.Inf_mem
added theorem is_compact.Sup_mem
added theorem is_compact.bdd_above
added theorem is_compact.bdd_below
added theorem is_compact.is_glb_Inf
added theorem is_compact.is_lub_Sup
deleted theorem compact.adherence_nhdset
deleted theorem compact.image
deleted theorem compact.inter_left
deleted theorem compact.inter_right
deleted theorem compact.prod
deleted theorem compact.union
deleted def compact
modified theorem compact_diff
modified theorem compact_empty
modified theorem compact_iff_compact_space
modified theorem compact_iff_compact_univ
modified theorem compact_singleton
modified theorem compact_univ
modified theorem compact_univ_pi
modified theorem generalized_tube_lemma
added theorem is_compact.image
added theorem is_compact.inter_left
added theorem is_compact.inter_right
added theorem is_compact.prod
added theorem is_compact.union
added def is_compact
deleted theorem set.finite.compact
added theorem set.finite.is_compact