image_preimage_eq_of_subset

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_preimage_eq_of_subset

English

If s ⊆ range f, then f''(f^{-1}(s)) = s.

Русский

Если s ⊆ range(f), то f''(f^{-1}(s)) = s.

LaTeX

$$$ s \\subseteq \\mathrm{range}(f) \\Rightarrow \\mathrm{image}(f)(\\mathrm{preimage}(f,s)) = s. $$$

Lean4

theorem image_preimage_eq_of_subset {f : α → β} {s : Set β} (hs : s ⊆ range f) : f '' (f ⁻¹' s) = s := by grind

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

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

Разделы

Аффилиация

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