Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-16 19:33 e3c9fd8d

View on Github →

feat(topology): sequential compactness (#3061) This is the long overdue PR bringing Bolzano-Weierstrass to mathlib. I'm sorry it's a bit large. I did use a couple of preliminary PRs, that one is really about converging subsequences, but supporting material is spread in many files.

Estimated changes

Modified src/data/nat/basic.lean

added def nat.strong_rec_on'

added theorem nat.strong_rec_on_beta'

Modified src/data/set/finite.lean

added theorem set.seq_of_forall_finite_exists

Modified src/data/set/lattice.lean

added theorem set.bUnion_mono

added theorem set.bUnion_subset_bUnion

Modified src/order/basic.lean

added theorem strict_mono.id_le

Modified src/order/filter/bases.lean

added theorem filter.is_countably_generated.subseq_tendsto

Modified src/order/filter/basic.lean

added theorem filter.exists_le_of_tendsto_at_top

added theorem filter.exists_lt_of_tendsto_at_top

added theorem filter.extraction_of_eventually_at_top

added theorem filter.extraction_of_frequently_at_top'

added theorem filter.extraction_of_frequently_at_top

added theorem filter.frequently_high_scores

added theorem filter.frequently_of_forall

added theorem filter.high_scores

added theorem filter.strict_mono_subseq_of_id_le

added theorem filter.strict_mono_subseq_of_tendsto_at_top

added theorem filter.strict_mono_tendsto_at_top

Modified src/tactic/monotonicity/lemmas.lean

Modified src/topology/bases.lean

added theorem topological_space.first_countable_topology.tendsto_subseq

Modified src/topology/metric_space/basic.lean

added theorem metric.ball_eq_ball'

added theorem metric.ball_eq_ball

added theorem metric.bounded_closure_of_bounded

added theorem metric.finite_approx_of_totally_bounded

modified theorem metric.totally_bounded_of_finite_discretization

Modified src/topology/sequences.lean

added theorem compact.seq_compact

added theorem compact.tendsto_subseq'

added theorem compact.tendsto_subseq

added theorem compact_space.tendsto_subseq

added theorem lebesgue_number_lemma_seq

added theorem metric.compact_iff_seq_compact

added theorem metric.compact_space_iff_seq_compact_space

added theorem seq_compact.lebesgue_number_lemma_of_metric

added theorem seq_compact.subseq_of_frequently_in

added theorem seq_compact.totally_bounded

added def seq_compact

added theorem seq_compact_space.tendsto_subseq

added theorem tendsto_subseq_of_bounded

added theorem tendsto_subseq_of_frequently_bounded

added theorem uniform_space.compact_space_iff_seq_compact_space

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean

added theorem cauchy_seq.mem_entourage

added theorem totally_bounded_of_forall_symm