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

Modified src/analysis/convex/topology.lean

modified theorem compact_std_simplex

Modified src/measure_theory/lebesgue_measure.lean

modified theorem real.volume_lt_top_of_compact

Modified src/topology/algebra/group.lean

modified theorem compact_covered_by_mul_left_translates

modified theorem compact_open_separated_mul

Modified src/topology/algebra/ordered.lean

deleted theorem compact.Inf_mem

deleted theorem compact.Sup_mem

deleted theorem compact.bdd_above

deleted theorem compact.bdd_below

deleted theorem compact.exists_Inf_image_eq

deleted theorem compact.exists_Sup_image_eq

deleted theorem compact.exists_forall_ge

deleted theorem compact.exists_forall_le

deleted theorem compact.exists_is_glb

deleted theorem compact.exists_is_greatest

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.exists_Inf_image_eq

added theorem is_compact.exists_Sup_image_eq

added theorem is_compact.exists_forall_ge

added theorem is_compact.exists_forall_le

added theorem is_compact.exists_is_glb

added theorem is_compact.exists_is_greatest

added theorem is_compact.exists_is_least

added theorem is_compact.exists_is_lub

added theorem is_compact.is_glb_Inf

added theorem is_compact.is_greatest_Sup

added theorem is_compact.is_least_Inf

added theorem is_compact.is_lub_Sup

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/compact_open.lean

Modified src/topology/compacts.lean

modified def topological_space.compacts

modified def topological_space.nonempty_compacts

modified def topological_space.positive_compacts:

Modified src/topology/homeomorph.lean

modified theorem homeomorph.compact_image

modified theorem homeomorph.compact_preimage

Modified src/topology/instances/real.lean

modified theorem compact_Icc

Modified src/topology/metric_space/basic.lean

modified theorem metric.bounded_of_compact

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/emetric_space.lean

modified theorem emetric.countable_closure_of_compact

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/separation.lean

deleted theorem compact.binary_compact_cover

deleted theorem compact.finite_compact_cover

deleted theorem compact.inter

deleted theorem compact.is_closed

added theorem is_compact.binary_compact_cover

added theorem is_compact.finite_compact_cover

added theorem is_compact.inter

added theorem is_compact.is_closed

modified theorem locally_compact_of_compact_nhds

Modified src/topology/sequences.lean

deleted theorem compact.seq_compact

deleted theorem compact.tendsto_subseq'

deleted theorem compact.tendsto_subseq

added theorem is_compact.is_seq_compact

added theorem is_compact.tendsto_subseq'

added theorem is_compact.tendsto_subseq

added theorem is_seq_compact.subseq_of_frequently_in

added theorem is_seq_compact.totally_bounded

added def is_seq_compact

modified theorem metric.compact_iff_seq_compact

deleted theorem seq_compact.subseq_of_frequently_in

deleted theorem seq_compact.totally_bounded

deleted def seq_compact

Modified src/topology/subset_properties.lean

deleted theorem compact.adherence_nhdset

deleted theorem compact.elim_finite_subcover

deleted theorem compact.elim_finite_subcover_image

deleted theorem compact.elim_finite_subfamily_closed

deleted theorem compact.image

deleted theorem compact.image_of_continuous_on

deleted theorem compact.inter_left

deleted theorem compact.inter_right

deleted theorem compact.nonempty_Inter_of_directed_nonempty_compact_closed

deleted theorem compact.nonempty_Inter_of_sequence_nonempty_compact_closed

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.adherence_nhdset

added theorem is_compact.elim_finite_subcover

added theorem is_compact.elim_finite_subcover_image

added theorem is_compact.elim_finite_subfamily_closed

added theorem is_compact.image

added theorem is_compact.image_of_continuous_on

added theorem is_compact.inter_left

added theorem is_compact.inter_right

added theorem is_compact.nonempty_Inter_of_directed_nonempty_compact_closed

added theorem is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed

added theorem is_compact.prod

added theorem is_compact.union

added def is_compact

modified theorem nhds_contain_boxes_of_compact

deleted theorem set.finite.compact

added theorem set.finite.is_compact

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean

Modified src/topology/uniform_space/compact_separated.lean

deleted theorem compact.uniform_continuous_on_of_continuous'

deleted theorem compact.uniform_continuous_on_of_continuous

added theorem is_compact.uniform_continuous_on_of_continuous'

added theorem is_compact.uniform_continuous_on_of_continuous