English
Version of composition for polynomial-on sets: if g is polynomial on t via image f and f is polynomial on s, then g ∘ f is polynomial on s.
Русский
Версия композиции для полиномов на множествах: если g полином на t через образ f и f полином на s, то g ∘ f полином на s.
LaTeX
$$$CPolynomialOn 𝕜 g t \\land CPolynomialOn 𝕜 f s \\Rightarrow CPolynomialOn 𝕜 (g \\circ f) s$$$
Lean4
/-- If two functions `g` and `f` are continuously polynomial respectively on `s.image f` and `s`,
then `g ∘ f` is continuously polynomial on `s`. -/
theorem comp' {s : Set E} {g : F → G} {f : E → F} (hg : CPolynomialOn 𝕜 g (s.image f)) (hf : CPolynomialOn 𝕜 f s) :
CPolynomialOn 𝕜 (g ∘ f) s := fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)
