Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open.prod

Modification history

2020-10-07 21:39

src/topology/constructions.lean

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

Added is_open.prod View on Github →