Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-09 22:24 3e458e23

View on Github →

chore(topology/sequences): rename variables (#14631)

  • types X, Y;
  • sequence x : ℕ → X;
  • a point a : X;
  • sets s, t.

Estimated changes

modified theorem is_closed.is_seq_closed
modified theorem is_compact.is_seq_compact
modified theorem is_compact.tendsto_subseq'
modified theorem is_compact.tendsto_subseq
modified def is_seq_closed
modified theorem is_seq_closed_iff_is_closed
modified theorem is_seq_closed_of_def
modified def is_seq_compact
modified theorem lebesgue_number_lemma_seq
modified theorem mem_closure_iff_seq_limit
modified def seq_closure
modified theorem seq_closure_subset_closure
modified def seq_continuous
modified theorem subset_seq_closure
modified theorem tendsto_subseq_of_bounded