image_image

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Function.LeftInverse.image_image

English

Let g be a left inverse of f. Then for every subset s of α, the image under g of the image of s under f equals s.

Русский

Пусть g является левым обратным к f. Тогда для любого множества s ⊆ α выполняется: g''(f''s) = s.

LaTeX

$$$ g''(f''s) = s $$$

Lean4

theorem image_image {g : β → α} (h : LeftInverse g f) (s : Set α) : g '' (f '' s) = s := by
  rw [← image_comp, h.comp_eq_id, image_id]

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

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

Разделы

Аффилиация

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