image_preimage_eq_range_inter

Mathlib.Data.Set.Image

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

English

For any f: α → β and any t ⊆ β, f''(f^{-1}(t)) = range(f) ∩ t.

Русский

Для любой функции f: α → β и любого множества t ⊆ β выполняется f''(f^{-1}(t)) = range(f) ∩ t.

LaTeX

$$$ f''(f^{-1}(t)) = \\mathrm{range}(f) \\cap t. $$$

Lean4

theorem image_preimage_eq_range_inter {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = range f ∩ t := by grind

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

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

Разделы

Аффилиация

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