Union

Statistics

Metric	Count
Definitions	0
Theorems `inf'_biUnion`, `inf_biUnion`, `sup'_biUnion`, `sup_biUnion`, `sup_eq_biUnion`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`inf'_biUnion` 📖	mathematical	`Nonempty`	`inf'` `biUnion` `Nonempty.biUnion`	—	`sup'_biUnion`
`inf_biUnion` 📖	mathematical	—	`inf` `biUnion`	—	`sup_biUnion`
`sup'_biUnion` 📖	mathematical	`Nonempty`	`sup'` `biUnion` `Nonempty.biUnion`	—	`eq_of_forall_ge_iff` `Nonempty.biUnion` `forall_swap`
`sup_biUnion` 📖	mathematical	—	`sup` `biUnion`	—	`eq_of_forall_ge_iff` `forall_swap`
`sup_eq_biUnion` 📖	mathematical	—	`sup` `Finset` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot` `biUnion`	—	`ext` `mem_sup` `mem_biUnion`

---