Theorems · Theorem · order theory

Set.seq_of_forall_finite_exists

∀ {γ : Type u_1} {P : γ → Set γ → Prop},
  (∀ (t : Set γ), t.Finite → ∃ c, P c t) → ∃ u, ∀ (n : ℕ), P (u n) (u '' Set.Iio n)

If P is some relation between terms of γ and sets in γ, such that every finite set t : Set γ has some c : γ related to it, then there is a recursively defined sequence u in γ so u n is related to the image of {0, 1, ..., n-1} under u. (We use this later to show sequentially compact sets are totally bounded.)

Defined in

Mathlib.Data.Set.Finite.Basic

Cited by

2 results in Mathlib

Foundations

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