iInter_setOf — Mathlib

English

For a family of predicates P_i on α, the intersection over i of the sets {x ∈ α | P_i(x)} equals the set {x ∈ α | ∀ i, P_i(x)}.

Русский

Пусть P_i — семейство предикатов на α. Тогда ⋂_i { x ∈ α | P_i(x) } = { x ∈ α | ∀ i, P_i(x) }.

LaTeX

$$$$ \\bigcap_{i} \\{ x \\in \\alpha \\mid P_i(x) \\} = \\{ x \\in \\alpha \\mid \\forall i, P_i(x) \\} $$$$

Lean4

theorem iInter_setOf (P : ι → α → Prop) : ⋂ i, {x : α | P i x} = {x : α | ∀ i, P i x} :=
  by
  ext
  exact mem_iInter

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