Theorems · Theorem · combinatorics

Finset.rado_selection_subtype

∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Finset α) → (a : ↥s) → β ↑a),
  ∃ χ, ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g t (Set.inclusion hst x)

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

1 results in Mathlib

Foundations

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

Assumes

Finite