Documentation

Mathlib.Data.Set.Accumulate

Accumulate #

The function Accumulate takes a set s and returns ⋃ y ≤ x, s y.

def Set.Accumulate {α : Type u_1} {β : Type u_2} [LE α] (s : αSet β) (x : α) :
Set β

Accumulate s is the union of s y for y ≤ x.

Equations
    Instances For
      theorem Set.accumulate_def {α : Type u_1} {β : Type u_2} {s : αSet β} [LE α] {x : α} :
      Accumulate s x = ⋃ (y : α), ⋃ (_ : y x), s y
      @[simp]
      theorem Set.mem_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [LE α] {x : α} {z : β} :
      z Accumulate s x yx, z s y
      theorem Set.subset_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] {x : α} :
      s x Accumulate s x
      theorem Set.accumulate_subset_iUnion {α : Type u_1} {β : Type u_2} {s : αSet β} [LE α] (x : α) :
      Accumulate s x ⋃ (i : α), s i
      theorem Set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] :
      theorem Set.accumulate_subset_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] {x y : α} (h : x y) :
      theorem Set.biUnion_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] (x : α) :
      ⋃ (y : α), ⋃ (_ : y x), Accumulate s y = ⋃ (y : α), ⋃ (_ : y x), s y
      theorem Set.iUnion_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] :
      ⋃ (x : α), Accumulate s x = ⋃ (x : α), s x
      @[simp]
      theorem Set.accumulate_bot {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] (s : αSet β) :
      @[simp]
      theorem Set.accumulate_zero_nat {β : Type u_2} (s : Set β) :
      Accumulate s 0 = s 0
      theorem Set.disjoint_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [Preorder α] (hs : Pairwise (Function.onFun Disjoint s)) {i j : α} (hij : i < j) :
      Disjoint (Accumulate s i) (s j)