Commit 2023-09-09 15:10 386927c1

View on Github →

feat: (sSup, Iic) and (Ici, sInf) are Galois connections (#6951)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.sUnion_powerset_gc

added def Set.sUnion_powerset_gi

added theorem Set.subset_powerset_iff

Modified Mathlib/Order/GaloisConnection.lean

added theorem gc_Ici_sInf

added theorem gc_sSup_Iic

added def gci_Ici_sInf

added def gi_sSup_Iic