Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-07 21:39 fa8b7ba2

View on Github →

chore(topology/*): use dot notation for is_open.prod and is_closed.prod (#4510)

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/special_functions/pow.lean

Modified src/topology/algebra/open_subgroup.lean

Modified src/topology/compact_open.lean

Modified src/topology/constructions.lean

added theorem is_closed.prod

deleted theorem is_closed_prod

added theorem is_open.prod

deleted theorem is_open_prod

Modified src/topology/instances/complex.lean

Modified src/topology/instances/real.lean

Modified src/topology/local_homeomorph.lean

Modified src/topology/topological_fiber_bundle.lean

Modified src/topology/uniform_space/compact_separated.lean