image_preimage_eq_iff

Mathlib.Data.Set.Image

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

English

For any f and s, f''(f^{-1}(s)) = s iff s ⊆ range f.

Русский

Для любой функции f и подмножества s верно: f''(f^{-1}(s)) = s тогда и только тогда, когда s ⊆ range f.

LaTeX

$$$ f''(f^{-1}(s)) = s \\iff s \\subseteq \\mathrm{range}(f). $$$

Lean4

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

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

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

Разделы

Аффилиация

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