instNonempty

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithUpper.instNonempty

English

If α is nonempty, then WithUpper α is nonempty.

Русский

Если α не пусто, то и WithUpper α не пусто.

LaTeX

$$$\\forall α,\\ \\mathrm{Nonempty}(α) \\Rightarrow \\mathrm{Nonempty}(\\mathrm{WithUpper} α)$$$

Lean4

instance [Nonempty α] : Nonempty (WithUpper α) :=
  ‹Nonempty α›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru