Theorems · Theorem · order theory

DFinsupp.lex_fibration

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop)
  [inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)],
  Relation.Fibration (InvImage (Prod.GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) Prod.snd) (DFinsupp.Lex r s)
    fun x => x.2.1.piecewise x.2.2 x.1

This key lemma says that if a finitely supported dependent function x₀ is obtained by merging two such functions x₁ and x₂, and if we evolve x₀ down the DFinsupp.Lex relation one step and get x, we can always evolve one of x₁ and x₂ down the DFinsupp.Lex relation one step while keeping the other unchanged, and merge them back (possibly in a different way) to get back x. In other words, the two parts evolve essentially independently under DFinsupp.Lex. This is used to show that a function x is accessible if DFinsupp.single i (x i) is accessible for each i in the (finite) support of x (DFinsupp.Lex.acc_of_single).

Defined in

Mathlib.Data.DFinsupp.WellFounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

ZeroDecidable