Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-23 19:57 fd7840ad

View on Github →

feat(topology/constructions): is_open_prod_iff' (#1454)

feat(topology/constructions): open_prod_iff'
reviewer's comments
fix build
golfed; is_open_map_fst

Estimated changes

Modified src/data/set/basic.lean

added theorem set.prod_subset_prod_iff

Modified src/topology/constructions.lean

added theorem is_open_map_fst

added theorem is_open_map_snd

added theorem is_open_prod_iff'