Theorems · Theorem · order theory

Set.exists_subset_accumulate_of_directed

∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) s → ∀ (n : ℕ), ∃ m, Set.accumulate s n ⊆ s m

For a directed set of sets s : ℕ → Set α and n : ℕ, there exists m : ℕ (maybe larger than n) such that accumulate s n ⊆ s m.

Defined in

Mathlib.Order.SetAccumulate

Cited by

1 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound