instTop — Mathlib

English

There exists a top element in the DefinableSet lattice over A, namely the entire space of functions α → M, which is definable by a universal condition.

Русский

Существует верхний элемент в полной части DefinableSet над A, а именно вся область функций α → M, задаваемая общим (универсальным) условием определимости.

LaTeX

$$$$ \\top_{(L, A, α)} \\text{ corresponds to } (α \\to M) \\text{ as a subset, i.e. } ((\\top : L.DefinableSet A α) : Set(α \\to M)) = \\mathrm{univ}. $$$$

Lean4

instance instTop : Top (L.DefinableSet A α) :=
  ⟨⟨⊤, definable_univ⟩⟩

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