Accumulate #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def set.accumulate {α : Type u_1} {β : Type u_2} [has_le α] (s : α → set β) (x : α) :

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

Equations

theorem set.accumulate_def {α : Type u_1} {β : Type u_2} {s : α → set β} [has_le α] {x : α} :

set.accumulate s x = ⋃ (y : α) (H : y ≤ x), s y

@[simp]

theorem set.mem_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [has_le α] {x : α} {z : β} :

z ∈ set.accumulate s x ↔ ∃ (y : α) (H : y ≤ x), z ∈ s y

theorem set.subset_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [preorder α] {x : α} :

theorem set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [preorder α] :

theorem set.bUnion_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [preorder α] (x : α) :

(⋃ (y : α) (H : y ≤ x), set.accumulate s y) = ⋃ (y : α) (H : y ≤ x), s y

theorem set.Union_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [preorder α] :

(⋃ (x : α), set.accumulate s x) = ⋃ (x : α), s x