biInter_eq_iInter — Mathlib

English

Let s be a set and t(x) a family of sets for x ∈ s. Then the intersection over x ∈ s of t x equals the intersection over x ∈ s considered as elements of the subtype, t x with x.2.

Русский

Пусть s — множество и t(x) — семейство множеств для x ∈ s. Тогда пересечение по x ∈ s равно пересечению по элементам подтипа x, t x с x.2.

LaTeX

$$$$ \\bigcap_{x \\in s} t(x) = \\bigcap_{x \\in s} t(x). $$$$

Lean4

theorem biInter_eq_iInter (s : Set α) (t : ∀ x ∈ s, Set β) : ⋂ x ∈ s, t x ‹_› = ⋂ x : s, t x x.2 :=
  iInf_subtype'

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