extendDomain — Mathlib

English

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

Русский

Пусть g отображает s в t; тогда отображение g.extendDomain f отображает (↑) ∘ f '' s в (↑) ∘ f '' t.

LaTeX

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

Lean4

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

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