comp_right

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.MapsTo.comp_right

English

For any f, MapsTo g s t implies MapsTo (g ∘ f) (f^{-1}(s)) t.

Русский

Если g отображает s в t, то g ∘ f отображает f^{-1}(s) в t.

LaTeX

$$$\\\\MapsTo g s t \\\\rightarrow \\\\MapsTo (\\\\circ g \\\\circ f) (f^{-1} s) t$$$

Lean4

theorem comp_right {s : Set β} {t : Set γ} (hg : MapsTo g s t) (f : α → β) : MapsTo (g ∘ f) (f ⁻¹' s) t := fun _ hx ↦
  hg hx

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

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

Разделы

Аффилиация

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