Accumulate #
The function Accumulate takes a set s and returns ⋃ y ≤ x, s y.
Accumulate s is the union of s y for y ≤ x.
Equations
- Eq (Set.Accumulate s x) (Set.iUnion fun (y : α) => Set.iUnion fun (h : LE.le y x) => s y)
Instances For
theorem
Set.mem_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[LE α]
{x : α}
{z : β}
:
Iff (Membership.mem (Accumulate s x) z) (Exists fun (y : α) => And (LE.le y x) (Membership.mem (s y) z))
theorem
Set.subset_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
{x : α}
:
HasSubset.Subset (s x) (Accumulate s x)
theorem
Set.accumulate_subset_iUnion
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[LE α]
(x : α)
:
HasSubset.Subset (Accumulate s x) (iUnion fun (i : α) => s i)
theorem
Set.monotone_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
:
Monotone (Accumulate s)
theorem
Set.accumulate_subset_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
{x y : α}
(h : LE.le x y)
:
HasSubset.Subset (Accumulate s x) (Accumulate s y)
theorem
Set.iUnion_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
:
Eq (iUnion fun (x : α) => Accumulate s x) (iUnion fun (x : α) => s x)
theorem
Set.accumulate_bot
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[OrderBot α]
(s : α → Set β)
:
Eq (Accumulate s Bot.bot) (s Bot.bot)
theorem
Set.disjoint_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
(hs : Pairwise (Function.onFun Disjoint s))
{i j : α}
(hij : LT.lt i j)
:
Disjoint (Accumulate s i) (s j)