preimage_preimage

Mathlib.Data.Set.Image

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

English

Let g be a left inverse of f. Then for every subset s, f^{-1}(g^{-1}(s)) = s.

Русский

Пусть g является левым обратным к f. Тогда для любого множества s: f^{-1}(g^{-1}(s)) = s.

LaTeX

$$$ f^{-1}(g^{-1}(s)) = s $$$

Lean4

theorem preimage_preimage {g : β → α} (h : LeftInverse g f) (s : Set α) : f ⁻¹' (g ⁻¹' s) = s := by
  rw [← preimage_comp, h.comp_eq_id, preimage_id]

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

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

Разделы

Аффилиация

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