Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.is_open_sUnion_countable

Modification history

2019-03-03 19:05

src/topology/bases.lean

chore(topology): Splits topology.basic and topology.continuity (#785) …

Modified topological_space.is_open_sUnion_countable View on Github →

2018-07-19 15:34

analysis/topology/topological_space.lean

feat(analysis/measure_theory): optimize proofs; trim, is_complete

Added topological_space.is_open_sUnion_countable View on Github →