fst_compEquiv_apply — Mathlib

English

The map on cotangent spaces induced by composition, Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom, is surjective.

Русский

Отображение котант пространства, индуцированное композицией, Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom, сюръективно.

LaTeX

$$$$ \forall y, \exists x : \mathrm{domain}(\mathrm{map}(Q.ofComp P))\; \mathrm{map}(Q.ofComp P)(x) = y. $$$$

Lean4

theorem fst_compEquiv_apply (x) : (compEquiv Q P x).1 = Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom x :=
  DFunLike.congr_fun (fst_compEquiv Q P) x

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