sym2_iInter

Mathlib.Data.Sym.Sym2

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

English

The sym2 of the infimum over i of f(i) equals the infimum over i of the sym2 of f(i).

Русский

Sym2 iInter: сим2 пересечения по i равен пересечению по i сим2-образов f(i).

LaTeX

$$$ (\bigcap_{i} f(i))^{\mathrm{sym2}} = \bigcap_{i} (f(i))^{\mathrm{sym2}} $$$

Lean4

theorem sym2_iInter {ι : Type*} (f : ι → Set α) : (⋂ i, f i).sym2 = ⋂ i, (f i).sym2 := by ext ⟨x, y⟩; simp [forall_and]

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

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

Разделы

Аффилиация

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