Commit 2023-02-14 05:07 6987cd5e

View on Github →

feat: port Topology.Sets.Compacts (#2265)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sets/Compacts.lean

added def TopologicalSpace.CompactOpens.Simps.coe

added theorem TopologicalSpace.CompactOpens.coe_bot

added theorem TopologicalSpace.CompactOpens.coe_compl

added theorem TopologicalSpace.CompactOpens.coe_inf

added theorem TopologicalSpace.CompactOpens.coe_map

added theorem TopologicalSpace.CompactOpens.coe_mk

added theorem TopologicalSpace.CompactOpens.coe_prod

added theorem TopologicalSpace.CompactOpens.coe_sdiff

added theorem TopologicalSpace.CompactOpens.coe_sup

added theorem TopologicalSpace.CompactOpens.coe_top

added def TopologicalSpace.CompactOpens.map

added def TopologicalSpace.CompactOpens.toClopens

added def TopologicalSpace.CompactOpens.toOpens

added structure TopologicalSpace.CompactOpens

added def TopologicalSpace.Compacts.Simps.coe

added theorem TopologicalSpace.Compacts.carrier_eq_coe

added theorem TopologicalSpace.Compacts.coe_bot

added theorem TopologicalSpace.Compacts.coe_finset_sup

added theorem TopologicalSpace.Compacts.coe_inf

added theorem TopologicalSpace.Compacts.coe_map

added theorem TopologicalSpace.Compacts.coe_mk

added theorem TopologicalSpace.Compacts.coe_prod

added theorem TopologicalSpace.Compacts.coe_sup

added theorem TopologicalSpace.Compacts.coe_top

added theorem TopologicalSpace.Compacts.equiv_to_fun_val

added structure TopologicalSpace.Compacts

added def TopologicalSpace.NonemptyCompacts.Simps.coe

added theorem TopologicalSpace.NonemptyCompacts.carrier_eq_coe

added theorem TopologicalSpace.NonemptyCompacts.coe_mk

added theorem TopologicalSpace.NonemptyCompacts.coe_prod

added theorem TopologicalSpace.NonemptyCompacts.coe_sup

added theorem TopologicalSpace.NonemptyCompacts.coe_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.coe_top

added def TopologicalSpace.NonemptyCompacts.toCloseds

added structure TopologicalSpace.NonemptyCompacts

added def TopologicalSpace.PositiveCompacts.Simps.coe

added theorem TopologicalSpace.PositiveCompacts.carrier_eq_coe

added theorem TopologicalSpace.PositiveCompacts.coe_mk

added theorem TopologicalSpace.PositiveCompacts.coe_prod

added theorem TopologicalSpace.PositiveCompacts.coe_sup

added theorem TopologicalSpace.PositiveCompacts.coe_toCompacts

added theorem TopologicalSpace.PositiveCompacts.coe_top

added theorem TopologicalSpace.PositiveCompacts.interior_nonempty

added def TopologicalSpace.PositiveCompacts.toNonemptyCompacts

added structure TopologicalSpace.PositiveCompacts

added theorem exists_positiveCompacts_subset