Absorbent

Mathlib.Topology.Bornology.Absorbs

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

English

A set is absorbent if it absorbs every singleton.

Русский

Множество Absorbent поглощает каждую одиночку.

LaTeX

$$$\operatorname{Absorbent}(s) \iff \forall x, \operatorname{Absorbs} M s \{x\}$$$

Lean4

/-- A set is *absorbent* if it absorbs every singleton. -/
def Absorbent (s : Set α) : Prop :=
  ∀ x, Absorbs M s { x }

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

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

Разделы

Аффилиация

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