instNonempty

Mathlib.Topology.UniformSpace.Completion

URI: https://scilib.ai/kg/mathlib#CauchyFilter.instNonempty

English

If α is nonempty, then CauchyFilter α is nonempty.

Русский

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

LaTeX

$$$\\text{Nonempty}(\\alpha)\\Rightarrow \\text{Nonempty}(\\mathrm{CauchyFilter}(\\alpha))$$$

Lean4

instance [h : Nonempty α] : Nonempty (CauchyFilter α) :=
  h.recOn fun a => Nonempty.intro <| CauchyFilter.pureCauchy a

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

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

Разделы

Аффилиация

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