iInter_setOf_subset — Mathlib

English

The intersection over i of {p : T.CompleteType α | S(i) ⊆ p} equals {p : T.CompleteType α | ⋃ i, S(i) ⊆ p}.

Русский

Пересечение по i множеств {p : T.CompleteType α | S(i) ⊆ p} равно множеству {p : T.CompleteType α | ⋃ i, S(i) ⊆ p}.

LaTeX

$$$\\\\big\\\\cap i : ι, {p : T.CompleteType α | S(i) \\\\subseteq p} = {p : T.CompleteType α | \\\\bigcup i : ι, S(i) \\\\subseteq p}$$$

Lean4

theorem iInter_setOf_subset {ι : Type*} (S : ι → L[[α]].Theory) :
    ⋂ i : ι, {p : T.CompleteType α | S i ⊆ p} = {p : T.CompleteType α | ⋃ i : ι, S i ⊆ p} :=
  by
  ext
  simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]

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