preimage_val_iInter

Mathlib.Data.Set.Subset

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

English

A ∩ ⋂ i s_i equals ⋂ i (A ∩ s_i).

Русский

A ∩ ⋂ i s_i = ⋂ i (A ∩ s_i).

LaTeX

$$$A \\cap \\bigcap_i s_i = \\bigcap_i (A \\cap s_i)$$$

Lean4

@[simp]
theorem preimage_val_iInter : A ↓∩ (⋂ i, s i) = ⋂ i, A ↓∩ s i :=
  preimage_iInter

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

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

Разделы

Аффилиация

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