Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 f53c776c

View on Github →

feat(analysis/topology): pi-spaces: topolopgy generation, prove second countability

Estimated changes

Modified analysis/topology/continuity.lean

added theorem is_open_set_pi

added theorem pi_eq_generate_from

added theorem pi_generate_from_eq

added theorem pi_generate_from_eq_fintype

Modified analysis/topology/topological_space.lean

added theorem generate_from_mono