Commit 2023-11-27 17:05 098e254c

View on Github →

feat(Data/Set/Lattice): generalize Set.iUnion_univ_pi (#8647) Allow ι : Type* to depend on a : α.

Estimated changes

modified theorem Set.iUnion_univ_pi