Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-10 09:00 dc788a0b

View on Github →

feat(topology/sequences): every first-countable space is sequential (#1528)

feat(topology/sequences): every first-countable space is sequential
fixup style
fixup comments
remove redundant type ascription

Estimated changes

Modified src/data/set/countable.lean

added theorem set.countable_iff_exists_surjective_to_subtype

Modified src/order/basic.lean

added theorem directed_of_mono

Modified src/order/complete_lattice.lean

added theorem lattice.infi_subtype'

Modified src/topology/bases.lean

added def filter.has_countable_basis

added theorem filter.has_countable_basis_iff_mono_seq

added theorem filter.has_countable_basis_iff_seq

added theorem filter.has_countable_basis_of_seq

added theorem filter.mono_seq_of_has_countable_basis

added theorem filter.seq_of_has_countable_basis

Modified src/topology/sequences.lean