mem_absorbing

Mathlib.Topology.Bornology.Absorbs

URI: https://scilib.ai/kg/mathlib#Filter.mem_absorbing

English

A set s belongs to absorbing G0 u if and only if Absorbs G0 s u.

Русский

Множество s принадлежит absorbing G0 u тогда, когда Absorbs G0 s u.

LaTeX

$$$s \in absorbing G_0 u \iff Absorbs G_0 s u$$$

Lean4

@[simp]
theorem mem_absorbing : s ∈ absorbing G₀ u ↔ Absorbs G₀ s u :=
  .rfl

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

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

Разделы

Аффилиация

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