postcomp — Mathlib

English

Postcomposition provides a way to obtain a solution on N from a solution on M using a linear map f: M → N.

Русский

Посткомпозиция задаёт решение на N из решения на M через линейное отображение f: M → N.

LaTeX

$$$\text{postcomp} : (\text{solutions on } M) \to (\text{solutions on } N)$ with $(\text{postcomp}_{f}(\text{solution})).\text{var } g = f(\text{solution.var } g)$$$

Lean4

/-- The image of a solution to `relations : Relation A` by a linear map `M →ₗ[A] N`. -/
@[simps]
def postcomp : relations.Solution N where
  var g := f (solution.var g)
  linearCombination_var_relation
    r := by
    have : Finsupp.linearCombination _ (fun g ↦ f (solution.var g)) = f.comp solution.π := by aesop
    simp [this]

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