Union

Statistics

Metric	Count
Definitions	0
Theorems `Ico_subset_biUnion_Ico`, `Ioc_subset_biUnion_Ioc`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`Ico_subset_biUnion_Ico` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.range`	—	`Set.Ico_eq_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.instReflSubset` `Set.Ico_subset_Ico_union_Ico` `Finset.range_add_one` `Set.iUnion_iUnion_eq_or_left` `Set.union_subset_union_right`
`Ioc_subset_biUnion_Ioc` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.range`	—	`Set.Ioc_eq_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.instReflSubset` `Set.Ioc_subset_Ioc_union_Ioc` `Finset.range_add_one` `Set.iUnion_iUnion_eq_or_left` `Set.union_subset_union_right`

---