Theorem Set.biUnion_le_eq_iUnion

Modification history

2026-08-24 10:14

Mathlib/Data/Set/Lattice.lean

refactor(Data/Set): split long file Lattice.lean (#43030) …

Modified Set.biUnion_le_eq_iUnion View on Github →

2024-10-22 22:22

Mathlib/Data/Set/Lattice.lean

feat: biSup, biInf, biUnion and biInter in NoMaxOrder (#17762)

Added Set.biUnion_le_eq_iUnion View on Github →