Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 11:48 4dd837dc

View on Github →

refactor(topology/sequences): redefine is_seq_closed, define Fréchet-Urysohn spaces (#15953)

  • redefine is_seq_closed as "the set contains every limit of a sequence of points from this set";
  • delete is_seq_closed_of_def and is_seq_closed.mem_of_tendsto, because now we use this property as the definition;
  • rename sequential_space to frechet_urysohn_space, add new sequential_space; this way our definitions agree with textbooks.

Estimated changes

deleted theorem is_closed.is_seq_closed
added theorem is_seq_closed.preimage
modified def is_seq_closed
added theorem is_seq_closed_iff
modified theorem is_seq_closed_iff_is_closed
deleted theorem is_seq_closed_of_def
modified theorem mem_closure_iff_seq_limit
added theorem seq_closure_eq_closure
modified theorem seq_closure_subset_closure
modified theorem subset_seq_closure