extendDomain — Mathlib

English

If SurjOn g s t, then SurjOn (g.extendDomain f) on the images ((↑) ∘ f)'' s to ((↑) ∘ f)'' t.

Русский

Если SurjOn g s t, то SurjOn (g.extendDomain f) на образах, полученных через f, сохраняется.

LaTeX

$$$ \\operatorname{SurjOn} g s t \\Rightarrow \\operatorname{SurjOn} (g.extendDomain f) ((↑) \\circ f '' s) ((↑) \\circ f '' t). $$$

Lean4

protected theorem extendDomain (h : SurjOn g s t) : SurjOn (g.extendDomain f) ((↑) ∘ f '' s) ((↑) ∘ f '' t) :=
  by
  rintro _ ⟨a, ha, rfl⟩
  obtain ⟨b, hb, rfl⟩ := h ha
  exact ⟨_, ⟨_, hb, rfl⟩, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

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