preimage_iInter

Mathlib.Data.Set.Lattice.Image

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

English

The preimage commutes with arbitrary intersections: the preimage of an intersection is the intersection of the preimages.

Русский

Прообраз пересечения равен пересечению прообразов.

LaTeX

$$$f^{-1}\left(\bigcap_i s_i\right) = \bigcap_i f^{-1}(s_i)$$$

Lean4

theorem preimage_iInter {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋂ i, s i) = ⋂ i, f ⁻¹' s i := by ext; simp

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

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

Разделы

Аффилиация

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