English
For l good with respect to π C (· ∈ s), the eval of l equals the evaluation via πJ composed with the evaluation on the π-projected space.
Русский
Если l хорош относительно π C (⋅ ∈ s), то eval(l) совпадает с eval, когда используем πJ и проекцию пространства π.
LaTeX
$$$\\forall I\\, C\\, [\\text{LinearOrder } I] \\ (s : Finset I)\\ (l : Profinite.NobelingProof.Products I)\\n (hl : l.isGood (π C (\\cdot ∈ s)))\\Rightarrow l.eval C = π_J C s \\big( l.eval (π C (\\cdot ∈ s))\\big).$$
Lean4
theorem eval_eq_πJ (l : Products I) (hl : l.isGood (π C (· ∈ s))) : l.eval C = πJ C s (l.eval (π C (· ∈ s))) :=
by
ext f
simp only [πJ, LocallyConstant.comapₗ, LinearMap.coe_mk, AddHom.coe_mk, LocallyConstant.coe_comap,
Function.comp_apply]
exact (congr_fun (Products.evalFacProp C (· ∈ s) (Products.prop_of_isGood C (· ∈ s) hl)) _).symm
