Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-27 04:33 d5d463e4

View on Github →

chore(topology/subset_properties): +2 lemmas about is_compact (#3567) Also use variables {s t : set α}

Estimated changes

Modified src/topology/subset_properties.lean

modified theorem cluster_point_of_compact

modified theorem compact_diff

modified theorem compact_iff_finite_subcover

modified theorem compact_iff_finite_subfamily_closed

modified theorem compact_iff_ultrafilter_le_nhds

modified theorem compact_of_finite_subcover

modified theorem compact_of_finite_subfamily_closed

modified theorem compact_of_is_closed_subset

modified theorem compact_univ_pi

modified theorem embedding.compact_iff_compact_image

modified theorem is_compact.adherence_nhdset

added theorem is_compact.compl_mem_sets

added theorem is_compact.compl_mem_sets_of_nhds_within

modified theorem is_compact.elim_finite_subcover

modified theorem is_compact.elim_finite_subcover_image

modified theorem is_compact.image

modified theorem is_compact.image_of_continuous_on

modified theorem is_compact.inter_left

modified theorem is_compact.inter_right

modified theorem is_compact.union

modified theorem set.finite.is_compact