English
The universal set on α is the set of all elements of α.
Русский
Вселенное множество на α — множество всех элементов α.
LaTeX
$$$\\mathrm{univ}:= \\{a \\in \\alpha \\mid \\; \\text{True}\\}$$$
Lean4
/-- The universal set on a type `α` is the set containing all elements of `α`.
This is conceptually the "same as" `α` (in set theory, it is actually the same), but type theory
makes the distinction that `α` is a type while `Set.univ` is a term of type `Set α`. `Set.univ` can
itself be coerced to a type `↥Set.univ` which is in bijection with (but distinct from) `α`. -/
def univ : Set α :=
{_a | True}
