Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 16:11 dab06b6b

View on Github →

refactor(topology/sequences): rename some sequential_ to seq_ (#14318)

Rename

  • sequential_closure → seq_closure, similarly rename lemmas;
  • sequentially_continuous → seq_continuous, similarly rename lemmas;
  • is_seq_closed_of_is_closed → is_closed.is_seq_closed;
  • mem_of_is_seq_closed → is_seq_closed.mem_of_tendsto;
  • continuous.to_sequentially_continuous → continuous.seq_continuous;

Remove

  • mem_of_is_closed_sequential: was a weaker version of is_closed.mem_of_tendsto;

Add

  • is_seq_closed.is_closed;
  • seq_continuous.continuous;

Estimated changes