Commit 2025-02-05 02:03 8827be0a
View on Github →feat(Data/Set/Lattice): iUnion + insertion (#21322)
Another distributivity lemma with iUnion and insertions, needed for #21172.
This could maybe be @[simp]
feat(Data/Set/Lattice): iUnion + insertion (#21322)
Another distributivity lemma with iUnion and insertions, needed for #21172.
This could maybe be @[simp]