preimage_union

Mathlib.Data.Set.Image

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

English

The preimage distributes over union: f^{-1}(s ∪ t) = f^{-1}(s) ∪ f^{-1}(t).

Русский

Обратное образ объединения равно объединению обратных образов.

LaTeX

$$$f^{-1}(s \cup t) = f^{-1}(s) \cup f^{-1}(t).$$$

Lean4

@[simp]
theorem preimage_union {s t : Set β} : f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t :=
  rfl

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

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

Разделы

Аффилиация

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