biUnion_eq_iUnion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem biUnion_eq_iUnion (s : Set α) (t : ∀ x ∈ s, Set β) : ⋃ x ∈ s, t x ‹_› = ⋃ x : s, t x x.2 :=
  iSup_subtype'

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