Commit 2024-06-25 14:51 27a0278f

View on Github →

feat(Topology/Sequences): add missing instances (#13460)

  • Subtype of a Fréchet-Urysohn space is a Fréchet-Urysohn space;
  • Disjoint union (Sum, Sigma) of sequential spaces is a sequential space.

Estimated changes

added theorem isClosed_coinduced