π_desc_apply — Mathlib

English

For all s and x, applying desc to s and then evaluating at x via solution.π yields s.π x.

Русский

Для всех s и x применение desc к s и последующая обработка через solution.π дают s.π x.

LaTeX

$$$$ h.desc\\, s (solution.\\pi\\, x) = s.\\pi\\, x $$$$

Lean4

@[simp]
theorem π_desc_apply (s : relations.Solution N) (x : relations.G →₀ A) : h.desc s (solution.π x) = s.π x :=
  DFunLike.congr_fun (h.desc_comp_π s) x

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