Theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq

Modification history

2026-10-10 09:42
Mathlib/Topology/Bases.lean
chore: delete deprecated declarations to March 2026 (#44240)
Deleted TopologicalSpace.FirstCountableTopology.tendsto_subseqView on Github →
2026-09-15 20:19
Mathlib/Topology/Bases.lean
chore: bump toolchain to v4.35.0-rc1 (#43843)
Modified TopologicalSpace.FirstCountableTopology.tendsto_subseqView on Github →
2026-04-03 17:21
Mathlib/Topology/Bases.lean
feat(Topology/Order): existence of a sequence that converges to limsup (#37296) …
Modified TopologicalSpace.FirstCountableTopology.tendsto_subseqView on Github →
2023-02-01 00:30
Mathlib/Topology/Bases.lean
feat: port Topology.Bases (#1910)
Added TopologicalSpace.FirstCountableTopology.tendsto_subseqView on Github →