English
If f : m → n is surjective, then the precomposition map (· ∘ f): (n → X) → (m → X) is an embedding; i.e., it is an injective inducing map with respect to the product topologies.
Русский
Если f: m → n сюръективно, то отображение предваренного композиционирования (g ↦ g ∘ f) из функций n → X в функции m → X является вложенным биином пространством (встраиванием).
LaTeX
$$$\\text{IsEmbedding}((\\cdot \\circ f)):\\, (n \\to X) \\to (m \\to X)\\quad\\text{при } f:\\; m \\to n \\text{ сюръективно}$$$
Lean4
theorem isEmbedding_comp {n m : Type*} (f : m → n) (hf : Function.Surjective f) :
IsEmbedding ((· ∘ f) : (n → X) → (m → X)) :=
by
refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩
simp only [nhds_pi, Filter.pi, Filter.comap_iInf, ← hf.iInf_congr, Filter.comap_comap, Function.comp_def]
