absorbs

Mathlib.Topology.Bornology.Absorbs

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

English

If a set s is absorbent with respect to a Bornology, then every singleton {x} is absorbed by s for all x.

Русский

Если множество s поглощающее относительно борологии, то для каждого x множество {x} поглощается s.

LaTeX

$$$Absorbent M s \\Rightarrow \\forall x,\, Absorbs M s \\{ x \\}$$$

Lean4

protected theorem absorbs (hs : Absorbent M s) {x : α} : Absorbs M s { x } :=
  hs x

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

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

Разделы

Аффилиация

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