Gluing functions along ordered finite subsets

Main definitions

• Finset.glue: join two functions along a subset and its complement, each enumerated by Mathlib's Finset.orderEmbOfFin.

Main results

• Finset.forall_iff_orderEmbOfFin_and_compl: split a predicate over the two enumerations.
• Finset.eq_glue_iff, Finset.glue_inj: reconstruction and uniqueness.
• Finset.eq_glue_of_reconstruct: reconstruct values through maps on the two parts.

References

Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. These are finite mathematical counts and identities; they give no native program or instruction-cost certificate.

theorem Finset.card_compl_of_card_eq {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) : Qᶜ.card = L - m

The complement of a size-m subset of Fin L has size L - m.

Predicates on a subset and its complement

theorem Finset.forall_iff_orderEmbOfFin_and_compl {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {P : Fin L → Prop} : (∀ (ℓ : Fin L), P ℓ) ↔ (∀ (k : Fin m), P ((Q.orderEmbOfFin hQ) k)) ∧ ∀ (k : Fin (L - m)), P ((Qᶜ.orderEmbOfFin ⋯) k)

A predicate holds everywhere if and only if it holds on the ordered enumerations of Q and its complement.

theorem Finset.filter_eq_iff_orderEmbOfFin_and_compl {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {P : Fin L → Prop} [DecidablePred P] : filter P univ = Q ↔ (∀ (k : Fin m), P ((Q.orderEmbOfFin hQ) k)) ∧ ∀ (k : Fin (L - m)), ¬P ((Qᶜ.orderEmbOfFin ⋯) k)

A predicate cuts out Q if and only if it holds on its ordered enumeration and fails on the ordered enumeration of its complement.

theorem Finset.filter_eq_of_forall_orderEmbOfFin {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {P : Fin L → Prop} [DecidablePred P] (hin : ∀ (k : Fin m), P ((Q.orderEmbOfFin hQ) k)) (hcard : (filter P univ).card = m) : filter P univ = Q

A predicate holding on every enumerated element of Q, and on m elements in all, cuts out Q.

Gluing functions along an ordered subset

def Finset.glue {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (f : Fin m → α) (g : Fin (L - m) → α) : Fin L → α

The function taking the values of f on Q and of g on its complement, with each part enumerated in increasing order.

@[simp]

theorem Finset.glue_orderEmbOfFin {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (f : Fin m → α) (g : Fin (L - m) → α) (k : Fin m) : Q.glue hQ f g ((Q.orderEmbOfFin hQ) k) = f k

Evaluating a glued function on the ordered enumeration of Q reads f.

@[simp]

theorem Finset.glue_orderEmbOfFin_compl {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (f : Fin m → α) (g : Fin (L - m) → α) (k : Fin (L - m)) : Q.glue hQ f g ((Qᶜ.orderEmbOfFin ⋯) k) = g k

Evaluating a glued function on the ordered enumeration of the complement reads g.

theorem Finset.glue_orderEmbOfFin_of_eq {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (f : Fin m → α) (g : Fin (L - m) → α) {Q' : Finset (Fin L)} (h : Q' = Q) (hQ' : Q'.card = m) (k : Fin m) : Q.glue hQ f g ((Q'.orderEmbOfFin hQ') k) = f k

Enumerating a subset equal to Q reads the same values from a glued function.

theorem Finset.glue_orderEmbOfFin_compl_of_eq {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (f : Fin m → α) (g : Fin (L - m) → α) {Q' : Finset (Fin L)} (h : Q' = Q) (hQ' : Q'.card = m) (k : Fin (L - m)) : Q.glue hQ f g ((Q'ᶜ.orderEmbOfFin ⋯) k) = g k

Enumerating the complement of a subset equal to Q reads the same values from a function glued along Q.

theorem Finset.eq_glue_iff {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} {f : Fin m → α} {g : Fin (L - m) → α} {u : Fin L → α} : u = Q.glue hQ f g ↔ (∀ (k : Fin m), u ((Q.orderEmbOfFin hQ) k) = f k) ∧ ∀ (k : Fin (L - m)), u ((Qᶜ.orderEmbOfFin ⋯) k) = g k

A function is the glued function exactly when its restrictions to both ordered parts have the stated values.

theorem Finset.glue_inj {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} {f f' : Fin m → α} {g g' : Fin (L - m) → α} : Q.glue hQ f g = Q.glue hQ f' g' ↔ f = f' ∧ g = g'

Both component functions can be read off their glued function.

theorem Finset.map_glue {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} {f : Fin m → α} {g : Fin (L - m) → α} {β : Type u_2} (φ : α → β) : (fun (ℓ : Fin L) => φ (Q.glue hQ f g ℓ)) = Q.glue hQ (fun (k : Fin m) => φ (f k)) fun (k : Fin (L - m)) => φ (g k)

Applying a map to a glued function maps both of its components.

Predicates and reconstruction on the two parts

theorem Finset.filter_glue {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} {f : Fin m → α} {g : Fin (L - m) → α} (P : α → Prop) [DecidablePred P] (hf : ∀ (k : Fin m), P (f k)) (hg : ∀ (k : Fin (L - m)), ¬P (g k)) : {ℓ : Fin L | P (Q.glue hQ f g ℓ)} = Q

If P holds on the values of f and fails on the values of g, it holds on the glued function exactly at the elements of Q.

theorem Finset.eq_glue_of_reconstruct {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) {α : Type u_1} (P : α → Prop) [DecidablePred P] {β : Type u_2} {γ : Type u_3} {fromSubset : β → α} {fromCompl : γ → α} {toSubset : α → β} {toCompl : α → γ} (hsubset : ∀ (a : α), P a → fromSubset (toSubset a) = a) (hcompl : ∀ (a : α), ¬P a → fromCompl (toCompl a) = a) {u : Fin L → α} (hu : {ℓ : Fin L | P (u ℓ)} = Q) : u = Q.glue hQ (fun (k : Fin m) => fromSubset (toSubset (u ((Q.orderEmbOfFin hQ) k)))) fun (k : Fin (L - m)) => fromCompl (toCompl (u ((Qᶜ.orderEmbOfFin ⋯) k)))

Reconstruct u from maps that recover its values on the subset defined by P and on its complement. The two reconstruction hypotheses apply on their respective parts.