nonempty_of_not_isMeagre

Mathlib.Topology.GDelta.Basic

URI: https://scilib.ai/kg/mathlib#nonempty_of_not_isMeagre

← MathLib Explorer

English

A set of second category (i.e. non-meagre) is nonempty.

Русский

Множество второй категории не пусто.

LaTeX

$$nonempty_of_not_isMeagre : (¬IsMeagre(s)) → s.Nonempty$$

Lean4

/-- A set of second category (i.e. non-meagre) is nonempty. -/
theorem nonempty_of_not_isMeagre {s : Set X} (hs : ¬IsMeagre s) : s.Nonempty :=
  by
  contrapose! hs
  simpa [hs] using IsMeagre.empty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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