image_preimage_eq_inter_range

Mathlib.Data.Set.Image

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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