comp_left

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.SurjOn.comp_left

English

If f maps s onto t, then for any g, g ∘ f maps s onto g''t.

Русский

Если f отображает s на t, то для любого g, g ∘ f отображает s на g''t.

LaTeX

$$$ \mathrm{SurjOn} f s t \rightarrow \mathrm{SurjOn}(g\circ f) s (g''t) $$$

Lean4

theorem comp_left (hf : SurjOn f s t) (g : β → γ) : SurjOn (g ∘ f) s (g '' t) := by rw [SurjOn, image_comp g f];
  exact image_mono hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru