comp_aeval_relation_inl — Mathlib

English

The aeval of the left-injected relation in the composed presentation equals the left-hand relation Q.relation r.

Русский

Оценка выражения в левой части композиции даёт то же самое, что Q.relation r.

LaTeX

$$$\\forall r:\\sigma',\\; \\mathrm{aeval}\\; (\\mathrm{Sum.elim}\\; X\\ (MvPolynomial.C \\circ P.val))\\ ((Q.comp P).relation(\\mathrm{Sum.inl}\\; r)) = Q.relation\\; r$$$

Lean4

theorem comp_aeval_relation_inl (r : σ') :
    aeval (Sum.elim X (MvPolynomial.C ∘ P.val)) ((Q.comp P).relation (Sum.inl r)) = Q.relation r :=
  by
  change (Q.aux P) _ = _
  simp [comp_relation, comp_relation_aux_map]

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