lex_fibration — Mathlib

English

Let x1 and x2 be finitely supported dependent functions whose merge is x. If one step of the Lex evolution from the merge produces x, then one can evolve either x1 or x2 by one Lex step while keeping the other fixed, and merge them back to recover x.

Русский

Пусть x1 и x2 — функции с конечной поддержкой, объединение которых даёт x. Если при одном шаге эволюции по порядку Lex от объединения получается x, тогда можно продвинуть либо x1, либо x2 на один шаг Lex, зафиксировать другую часть и вернуть их объединением к x.

LaTeX

$$$\\mathrm{Fibration}\\big(\\mathrm{InvImage}\\big(\\mathrm{GameAdd}(\\mathrm{DFinsupp.Lex}(r,s),\\,\\mathrm{DFinsupp.Lex}(r,s))\\,\\mathrm{snd}\\big),\\; \\mathrm{DFinsupp.Lex}(r,s),\\; \\lambda x.\\ \\mathrm{piecewise}(x.2.1,\\ x.2.2,\\ x.1)\\big)$$$

Lean4

/-- 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`). -/
theorem lex_fibration [∀ (i) (s : Set ι), Decidable (i ∈ s)] :
    Fibration (InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd) (DFinsupp.Lex r s) fun x =>
      piecewise x.2.1 x.2.2 x.1 :=
  by
  rintro ⟨p, x₁, x₂⟩ x ⟨i, hr, hs⟩
  simp_rw [piecewise_apply] at hs hr
  split_ifs at hs with hp
  · refine ⟨⟨{j | r j i → j ∈ p}, piecewise x₁ x {j | r j i}, x₂⟩, .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;>
      simp only [piecewise_apply, Set.mem_setOf_eq]
    · simp only [if_pos hj]
    · split_ifs with hi
      · rwa [hr i hi, if_pos hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_setOf_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₂, if_pos (h₁ h₂)]
      · rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]
  · refine ⟨⟨{j | r j i ∧ j ∈ p}, x₁, piecewise x₂ x {j | r j i}⟩, .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;>
      simp only [piecewise_apply, Set.mem_setOf_eq]
    · exact if_pos hj
    · split_ifs with hi
      · rwa [hr i hi, if_neg hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_setOf_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₁.1, if_pos h₁.2]
      · rw [hr j h₂, if_neg]
        simpa [h₂] using h₁

Похожие утверждения