map — Mathlib

English

If h is a equation on W', then its image under f via map corresponds to the equation of the mapped object with argument f ∘ P.

Русский

Если h — уравнение на W', то его образ под действием отображения через map соответствует уравнению отображённого объекта с аргументом f ∘ P.

LaTeX

$$$$\\text{map}(h) : (W'.\\mathrm{map} f).\\mathrm{toJacobian}.\\mathrm{Equation}(f \\circ P) = h$$$$

Lean4

theorem map (h : W'.Equation P) : (W'.map f).toJacobian.Equation (f ∘ P) := by
  rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]

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