Theorems · Theorem · combinatorics

Finset.rado_selection

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

Given a (dependent) function g s : (a : α) → β a for each finset 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

2 results in Mathlib

Foundations

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

Assumes

Finite