setOf_forall

Mathlib.Data.Set.Lattice

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

English

The set of x such that ∀ i, p(i, x) holds equals the intersection of the sets {x | p(i, x)} over i.

Русский

Множество x таких, что для всех i выполняется p(i, x), равно пересечению множеств {x | p(i, x)} по i.

LaTeX

$${x | ∀ i, p(i, x)} = ⋂ i, {x | p(i, x)}$$

Lean4

theorem setOf_forall (p : ι → β → Prop) : {x | ∀ i, p i x} = ⋂ i, {x | p i x} :=
  ext fun _ => mem_iInter.symm

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

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

Разделы

Аффилиация

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