comp — Mathlib

English

Version of the polynomial-on-sets composition with mappings: if g is polynomial on t, f is polynomial on s, and f maps s into t, then g ∘ f is polynomial on s.

Русский

Версия композиции полиномонов на множествах с отображениями: если g полином на t, f полином на s, и f(s) ⊆ t, тогда g ∘ f полином на s.

LaTeX

$$$CPolynomialOn 𝕜 g t \\land CPolynomialOn 𝕜 f s \\land Set.MapsTo f s t \\Rightarrow CPolynomialOn 𝕜 (g \\circ f) s$$$

Lean4

theorem comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : CPolynomialOn 𝕜 g t) (hf : CPolynomialOn 𝕜 f s)
    (st : Set.MapsTo f s t) : CPolynomialOn 𝕜 (g ∘ f) s :=
  comp' (mono hg (Set.mapsTo_iff_image_subset.mp st)) hf

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