Theorems · Theorem · combinatorics

Set.Finite.rado_selection

∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Set α) → s.Finite → (a : α) → β a),
  ∃ χ, ∀ (s : Set α), s.Finite → ∃ t, ∃ (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Given a (dependent) function g s : (a : α) → β a for each finite set s of α, provided that each β a is finite, we can find another function χ : (a : α) → β a such that on every s, there is some larger t such that χ agrees with g t on s. Informally, we are stitching together the local functions g s into a global χ such that on each s, χ can be expressed in terms of one of the g.

Defined in

Mathlib.Combinatorics.Compactness

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite