mathlib
dab06b6b - refactor(topology/sequences): rename some `sequential_` to `seq_` (#14318)

Commit
3 years ago
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`;
Author
Parents
Loading