sigma — Mathlib

English

Definition of the indexed sum Set.sigma(s,t) as the set of dependent pairs (i,a) with i in s and a in t i.

Русский

Определение индексированной суммы: множество σ(s,t) состоит из пар (i,a) с i ∈ s и a ∈ t(i).

LaTeX

$$$\\mathrm{Set}.sigma(s,t) = \\{ x \\mid x.1 \\in s \\land x.2 \\in t(x.1) \\}$$$

Lean4

/-- Indexed sum of sets. `s.sigma t` is the set of dependent pairs `⟨i, a⟩` such that `i ∈ s` and
`a ∈ t i`. -/
protected def sigma (s : Set ι) (t : ∀ i, Set (α i)) : Set (Σ i, α i) :=
  {x | x.1 ∈ s ∧ x.2 ∈ t x.1}

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