Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-18 08:49 e82fbd32

View on Github →

feat(topology/sets/closeds): The coframe of closed sets (#15338) coframe (closeds α).

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.Inter₂_union

added theorem set.union_Inter₂

Modified src/topology/sets/closeds.lean

added theorem topological_space.closeds.coe_Inf

added theorem topological_space.closeds.coe_infi

added theorem topological_space.closeds.gc

added def topological_space.closeds.gi

added theorem topological_space.closeds.infi_def

added theorem topological_space.closeds.infi_mk

added theorem topological_space.closeds.mem_Inf

added theorem topological_space.closeds.mem_infi

Modified src/topology/sets/opens.lean

modified theorem topological_space.opens.coe_Sup

added theorem topological_space.opens.coe_supr

deleted theorem topological_space.opens.supr_s

Modified src/topology/sheaves/sheaf_condition/equalizer_products.lean

Modified src/topology/sheaves/sheaf_condition/pairwise_intersections.lean