Commit 2023-02-11 21:16 c823841b

View on Github →

feat: port Topology.Sets.Closeds (#2216)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sets/Closeds.lean

added def TopologicalSpace.Clopens.Simps.coe

added theorem TopologicalSpace.Clopens.clopen

added theorem TopologicalSpace.Clopens.coe_bot

added theorem TopologicalSpace.Clopens.coe_compl

added theorem TopologicalSpace.Clopens.coe_inf

added theorem TopologicalSpace.Clopens.coe_mk

added theorem TopologicalSpace.Clopens.coe_sdiff

added theorem TopologicalSpace.Clopens.coe_sup

added theorem TopologicalSpace.Clopens.coe_top

added def TopologicalSpace.Clopens.toOpens

added structure TopologicalSpace.Clopens

added def TopologicalSpace.Closeds.Simps.coe

added theorem TopologicalSpace.Closeds.closed

added theorem TopologicalSpace.Closeds.coe_bot

added theorem TopologicalSpace.Closeds.coe_eq_empty

added theorem TopologicalSpace.Closeds.coe_eq_univ

added theorem TopologicalSpace.Closeds.coe_finset_inf

added theorem TopologicalSpace.Closeds.coe_finset_sup

added theorem TopologicalSpace.Closeds.coe_inf

added theorem TopologicalSpace.Closeds.coe_infᵢ

added theorem TopologicalSpace.Closeds.coe_infₛ

added theorem TopologicalSpace.Closeds.coe_mk

added theorem TopologicalSpace.Closeds.coe_nonempty

added theorem TopologicalSpace.Closeds.coe_sup

added theorem TopologicalSpace.Closeds.coe_top

added def TopologicalSpace.Closeds.compl

added def TopologicalSpace.Closeds.complOrderIso

added theorem TopologicalSpace.Closeds.compl_bijective

added theorem TopologicalSpace.Closeds.gc

added def TopologicalSpace.Closeds.gi

added theorem TopologicalSpace.Closeds.infᵢ_def

added theorem TopologicalSpace.Closeds.infᵢ_mk

added theorem TopologicalSpace.Closeds.isAtom_iff

added theorem TopologicalSpace.Closeds.mem_infᵢ

added theorem TopologicalSpace.Closeds.mem_infₛ

added def TopologicalSpace.Closeds.singleton

added structure TopologicalSpace.Closeds

added def TopologicalSpace.Opens.compl

added def TopologicalSpace.Opens.complOrderIso

added theorem TopologicalSpace.Opens.compl_bijective

added theorem TopologicalSpace.Opens.isCoatom_iff