Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 16:26 527afb3d

View on Github →

feat(topology/sets/compacts): prod constructions (#15118)

Estimated changes

Modified src/topology/sets/compacts.lean

added theorem topological_space.compact_opens.coe_prod

added theorem topological_space.compacts.carrier_eq_coe

added theorem topological_space.compacts.coe_prod

added theorem topological_space.nonempty_compacts.carrier_eq_coe

added theorem topological_space.nonempty_compacts.coe_prod

added theorem topological_space.positive_compacts.carrier_eq_coe

added theorem topological_space.positive_compacts.coe_prod