Commit 2022-03-05 01:51 17559112

View on Github →

feat(topology/compacts): The types of clopens and of compact opens (#11966) Define clopens and compact_opens, the types of clopens and of compact open sets of a topological space.

Estimated changes

Modified src/topology/compacts.lean

added theorem topological_space.clopens.clopen

added theorem topological_space.clopens.coe_bot

added theorem topological_space.clopens.coe_compl

added theorem topological_space.clopens.coe_inf

added theorem topological_space.clopens.coe_mk

added theorem topological_space.clopens.coe_sdiff

added theorem topological_space.clopens.coe_sup

added theorem topological_space.clopens.coe_top

added def topological_space.clopens.to_opens

added structure topological_space.clopens

added theorem topological_space.compact_opens.coe_bot

added theorem topological_space.compact_opens.coe_compl

added theorem topological_space.compact_opens.coe_inf

added theorem topological_space.compact_opens.coe_map

added theorem topological_space.compact_opens.coe_mk

added theorem topological_space.compact_opens.coe_sdiff

added theorem topological_space.compact_opens.coe_sup

added theorem topological_space.compact_opens.coe_top

added theorem topological_space.compact_opens.compact

added def topological_space.compact_opens.map

added def topological_space.compact_opens.to_clopens

added def topological_space.compact_opens.to_opens

added theorem topological_space.compact_opens.«open»

added structure topological_space.compact_opens