exists_pos

Mathlib.Analysis.LocallyConvex.Basic

URI: https://scilib.ai/kg/mathlib#Absorbs.exists_pos

← MathLib Explorer

English

If T is positive, then T is symmetric.

Русский

Если T положителен, то T симметричен.

LaTeX

$$$T\\text{ positive} \\Rightarrow T\\text{ symmetric}$$$

Lean4

theorem exists_pos (h : Absorbs 𝕜 A B) : ∃ r > 0, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A :=
  let ⟨r, hr₁, hr⟩ := (Filter.atTop_basis' 1).cobounded_of_norm.eventually_iff.1 h
  ⟨r, one_pos.trans_le hr₁, hr⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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