IsMeagre

Mathlib.Topology.GDelta.Basic

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

English

A set s is meagre iff its complement is residual.

Русский

Множество s мезгрей тогда и только тогда, когда его дополнение принадлежит резидуальному фильтру.

LaTeX

$$IsMeagre(s) \iff s^c ∈ residual(X)$$

Lean4

/-- A set is called **meagre** iff its complement is a residual (or comeagre) set. -/
def IsMeagre (s : Set X) :=
  sᶜ ∈ residual X

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

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

Разделы

Аффилиация

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