Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 21:43 366a23fb

View on Github →

feat(topology/constructions): frontier/interior/closure in X × Y (#6594)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.prod_diff_prod

Modified src/order/filter/basic.lean

added theorem filter.prod_mem_prod_iff

Modified src/topology/algebra/ordered.lean

added theorem frontier_Ici_subset

added theorem frontier_Iic_subset

Modified src/topology/basic.lean

added theorem frontier_empty

added theorem frontier_univ

Modified src/topology/constructions.lean

added theorem frontier_prod_eq

added theorem frontier_prod_univ_eq

added theorem frontier_univ_prod_eq

added theorem interior_prod_eq

added theorem prod_mem_nhds_iff