Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.Union_const

Modification history

2023-01-08 09:48
src/data/set/lattice.lean
feat(data/{set,finset}/basic): Convenience lemmas (#17957) …
Modified set.Union_constView on Github →
2021-08-11 02:38
src/data/set/lattice.lean
docs(data/set/lattice): add module docstring (#8250) …
Modified set.Union_constView on Github →
2021-02-28 17:40
src/data/set/lattice.lean
feat(data/set): more lemmas (#6474)
Modified set.Union_constView on Github →
2020-02-11 13:43
src/data/set/lattice.lean
feat(tactic/lint): check if inhabited instances should be nonempty (#1971) …
Modified set.Union_constView on Github →
2018-07-16 20:46
data/set/lattice.lean
feat(data/set/basic): more set theorems, normalize naming
Added set.Union_constView on Github →