absorbs_self

Mathlib.Analysis.LocallyConvex.Basic

URI: https://scilib.ai/kg/mathlib#Balanced.absorbs_self

English

A balanced set absorbs itself: s absorbs s.

Русский

Сбалансированное множество поглощает само себя: s абсорбирует s.

LaTeX

$$$\\text{Balanced } 𝕜 \\Rightarrow \\text{Absorbs } 𝕜 s s$$$

Lean4

/-- A balanced set absorbs itself. -/
theorem absorbs_self (hs : Balanced 𝕜 s) : Absorbs 𝕜 s s :=
  .of_norm ⟨1, fun _ => hs.subset_smul⟩

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

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

Разделы

Аффилиация

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