preimage_iUnion

Mathlib.Data.Set.Lattice.Image

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

English

For any function f and family s_i of sets, f^{-1}(⋃ i, s_i) = ⋃ i, f^{-1}(s_i).

Русский

Для любой функции f и семейства множеств s_i выполняется f^{-1}(⋃ i, s_i) = ⋃ i, f^{-1}(s_i).

LaTeX

$$$f^{-1}\Bigl(\bigcup_i s_i\Bigr) = \bigcup_i f^{-1}(s_i)$$$

Lean4

@[simp]
theorem preimage_iUnion {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋃ i, s i) = ⋃ i, f ⁻¹' s i :=
  Set.ext <| by simp [preimage]

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

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

Разделы

Аффилиация

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