Commit 2024-02-02 21:55 6daa3eb7

View on Github →

feat(Set/Lattice): upgrade some lemmas to iffs (#10181)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

modified theorem Set.mapsTo_iInter

modified theorem Set.mapsTo_iInter₂

modified theorem Set.mapsTo_iUnion

modified theorem Set.mapsTo_iUnion₂

modified theorem Set.mapsTo_sInter

modified theorem Set.mapsTo_sUnion

Modified Mathlib/Topology/Compactness/LocallyCompact.lean