sigmaToiUnion — Mathlib

English

sigmaToiUnion maps a dependent pair (a, x) with x ∈ t(a) to the element x in the union over all a of t(a).

Русский

sigmaToiUnion переводит зависимую пару (a, x) с x ∈ t(a) в элемент x в объединении ⋃ a t(a).

LaTeX

$$$$\\sigmaToiUnion : \\Sigma a, t(a) \\to \\bigcup_a t(a).$$$$

Lean4

/-- If `t` is an indexed family of sets, then there is a natural map from `Σ i, t i` to `⋃ i, t i`
sending `⟨i, x⟩` to `x`. -/
def sigmaToiUnion (x : Σ i, t i) : ⋃ i, t i :=
  ⟨x.2, mem_iUnion.2 ⟨x.1, x.2.2⟩⟩

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