English
Let X be a family of types X a indexed by α. The universe of dependent pairs (a, x) with x ∈ X a is the union over a of the graphs { (a, x) : x ∈ X a }. In symbols: univ = ⋃ a, range (Sigma.mk a).
Русский
Пусть X — семейство типов X a, индексированное по α. Вселенная зависимых пар (a, x) с x ∈ X a равна объединению по a графиков { (a, x) : x ∈ X a }. Обозначим: univ = ⋃ a, range (Sigma.mk a).
LaTeX
$$$$ \\operatorname{univ} = \\bigcup_{a} \\operatorname{range}(\\operatorname{Sigma.mk} a). $$$$
Lean4
theorem univ (X : α → Type*) : (Set.univ : Set (Σ a, X a)) = ⋃ a, range (Sigma.mk a) :=
Set.ext fun x => iff_of_true trivial ⟨range (Sigma.mk x.1), Set.mem_range_self _, x.2, Sigma.eta x⟩
