Mathlib.Data.Set.Accumulate

Set.Accumulate definition

[LE α] (s : α → Set β) (x : α) : Set β

Full source

/-- `Accumulate s` is the union of `s y` for `y ≤ x`. -/
def Accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
  ⋃ y ≤ x, s y

Accumulation of a family of sets

Informal description

Given a type $\alpha$ with a preorder $\leq$ and a family of sets $s : \alpha \to \text{Set } \beta$, the accumulation of $s$ at $x \in \alpha$ is the union of all sets $s(y)$ for $y \leq x$. In other words, $\text{Accumulate } s x = \bigcup_{y \leq x} s(y)$.

Set.accumulate_def theorem

[LE α] {x : α} : Accumulate s x = ⋃ y ≤ x, s y

Full source

theorem accumulate_def [LE α] {x : α} : Accumulate s x = ⋃ y ≤ x, s y :=
  rfl

Definition of Accumulate: $\text{Accumulate } s x = \bigcup_{y \leq x} s(y)$

Informal description

Given a type $\alpha$ with a preorder $\leq$ and a family of sets $s : \alpha \to \text{Set } \beta$, the accumulation of $s$ at $x \in \alpha$ is equal to the union of all sets $s(y)$ for $y \leq x$, i.e., \[ \text{Accumulate } s x = \bigcup_{y \leq x} s(y). \]

Set.mem_accumulate theorem

[LE α] {x : α} {z : β} : z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Full source

@[simp]
theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ Accumulate s xz ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by
  simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

Characterization of Membership in Accumulated Sets

Informal description

For a type $\alpha$ with a preorder $\leq$ and a family of sets $s : \alpha \to \text{Set } \beta$, an element $z \in \beta$ belongs to the accumulation of $s$ at $x \in \alpha$ if and only if there exists $y \in \alpha$ with $y \leq x$ such that $z \in s(y)$. In other words: $$ z \in \text{Accumulate } s x \iff \exists y \leq x, z \in s(y) $$

Set.subset_accumulate theorem

[Preorder α] {x : α} : s x ⊆ Accumulate s x

Full source

theorem subset_accumulate [Preorder α] {x : α} : s x ⊆ Accumulate s x := fun _ => mem_biUnion le_rfl

Inclusion of Set in Its Accumulation: $s(x) \subseteq \text{Accumulate } s x$

Informal description

For any type $\alpha$ with a preorder $\leq$ and any family of sets $s : \alpha \to \text{Set } \beta$, the set $s(x)$ is a subset of its accumulation at $x$, i.e., $s(x) \subseteq \bigcup_{y \leq x} s(y)$.

Set.accumulate_subset_iUnion theorem

[LE α] (x : α) : Accumulate s x ⊆ ⋃ i, s i

Full source

theorem accumulate_subset_iUnion [LE α] (x : α) : AccumulateAccumulate s x ⊆ ⋃ i, s i :=
  (biUnion_subset_biUnion_left (subset_univ _)).trans_eq (biUnion_univ _)

Accumulation is Subset of Union: $\text{Accumulate } s x \subseteq \bigcup_i s(i)$

Informal description

For any type $\alpha$ with a preorder $\leq$ and any family of sets $s : \alpha \to \text{Set } \beta$, the accumulation of $s$ at $x \in \alpha$ is a subset of the union of all sets in the family. In other words: \[ \text{Accumulate } s x \subseteq \bigcup_{i} s(i). \]

Set.monotone_accumulate theorem

[Preorder α] : Monotone (Accumulate s)

Full source

theorem monotone_accumulate [Preorder α] : Monotone (Accumulate s) := fun _ _ hxy =>
  biUnion_subset_biUnion_left fun _ hz => le_trans hz hxy

Monotonicity of the Accumulation Function

Informal description

For any type $\alpha$ with a preorder $\leq$ and any family of sets $s : \alpha \to \text{Set } \beta$, the accumulation function $\text{Accumulate } s$ is monotone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\text{Accumulate } s x \subseteq \text{Accumulate } s y$.

Set.accumulate_subset_accumulate theorem

[Preorder α] {x y} (h : x ≤ y) : Accumulate s x ⊆ Accumulate s y

Full source

@[gcongr]
theorem accumulate_subset_accumulate [Preorder α] {x y} (h : x ≤ y) :
    AccumulateAccumulate s x ⊆ Accumulate s y :=
  monotone_accumulate h

Monotonicity of Accumulation: $x \leq y \Rightarrow \text{Accumulate } s \, x \subseteq \text{Accumulate } s \, y$

Informal description

For any preorder $\alpha$ and any family of sets $s \colon \alpha \to \text{Set } \beta$, if $x \leq y$ in $\alpha$, then the accumulation of $s$ at $x$ is a subset of the accumulation of $s$ at $y$, i.e., \[ \text{Accumulate } s \, x \subseteq \text{Accumulate } s \, y. \]

Set.biUnion_accumulate theorem

[Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y

Full source

theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y := by
  apply Subset.antisymm
  · exact iUnion₂_subset fun y hy => monotone_accumulate hy
  · exact iUnion₂_mono fun y _ => subset_accumulate

Double Union Property of Accumulation: $\bigcup_{y \leq x} \text{Accumulate } s y = \bigcup_{y \leq x} s y$

Informal description

Let $\alpha$ be a type with a preorder $\leq$ and let $s : \alpha \to \text{Set } \beta$ be a family of sets. For any $x \in \alpha$, the union of all accumulations $\text{Accumulate } s y$ for $y \leq x$ equals the union of all sets $s(y)$ for $y \leq x$. In other words, $$\bigcup_{y \leq x} \left( \bigcup_{z \leq y} s(z) \right) = \bigcup_{y \leq x} s(y).$$

Set.iUnion_accumulate theorem

[Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x

Full source

theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x := by
  apply Subset.antisymm
  · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
    intro z x x' ⟨_, hz⟩
    exact ⟨x', hz⟩
  · exact iUnion_mono fun i => subset_accumulate

Union of Accumulations Equals Union of Original Sets

Informal description

For any preorder $\alpha$ and any family of sets $s \colon \alpha \to \text{Set } \beta$, the union of all accumulations of $s$ is equal to the union of all sets in $s$, i.e., $$\bigcup_{x \in \alpha} \text{Accumulate } s \, x = \bigcup_{x \in \alpha} s(x).$$

Set.accumulate_bot theorem

[PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥

Full source

@[simp]
lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥ := by
  simp [Set.accumulate_def]

Accumulation at Bottom Element Equals Value at Bottom

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot$, and let $s : \alpha \to \text{Set } \beta$ be a family of sets. Then the accumulation of $s$ at $\bot$ is equal to $s(\bot)$, i.e., $$\text{Accumulate } s \bot = s(\bot).$$

Set.accumulate_zero_nat theorem

(s : ℕ → Set β) : Accumulate s 0 = s 0

Full source

@[simp]
lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0 := by
  simp [accumulate_def]

Accumulation at Zero Equals Initial Set

Informal description

For any family of sets $s \colon \mathbb{N} \to \text{Set } \beta$, the accumulation of $s$ at $0$ is equal to $s(0)$, i.e., $$\text{Accumulate } s \, 0 = s(0).$$

Set.disjoint_accumulate theorem

[Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) : Disjoint (Accumulate s i) (s j)

Full source

theorem disjoint_accumulate [Preorder α] (hs : Pairwise (DisjointDisjoint on s)) {i j : α} (hij : i < j) :
    Disjoint (Accumulate s i) (s j) := by
  apply disjoint_left.2 (fun x hx ↦ ?_)
  simp only [Accumulate, mem_iUnion, exists_prop] at hx
  rcases hx with ⟨k, hk, hx⟩
  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Disjointness of Accumulation with Later Sets in Preorder

Informal description

Let $\alpha$ be a preorder and $s : \alpha \to \text{Set } \beta$ be a family of sets such that $s$ is pairwise disjoint (i.e., $s(i) \cap s(j) = \emptyset$ for all $i \neq j$). Then for any $i, j \in \alpha$ with $i < j$, the accumulation of $s$ up to $i$ is disjoint from $s(j)$, i.e., $$\left(\bigcup_{k \leq i} s(k)\right) \cap s(j) = \emptyset.$$