subset_smul

Mathlib.Analysis.LocallyConvex.Basic

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

English

If hs is balanced and 1 ≤ ‖a‖, then s ⊆ a · s.

Русский

Если s сбалансировано и 1 ≤ ‖a‖, то s ⊆ a · s.

LaTeX

$$$\\\\text{Balanced } 𝕝 \\\\Rightarrow \\\\ 1 \\\\le \\\\|a\\\\| \\\\Rightarrow s \\\\subseteq a \\\\cdot s$$$

Lean4

theorem subset_smul (hs : Balanced 𝕜 s) (ha : 1 ≤ ‖a‖) : s ⊆ a • s := by rw [← @norm_one 𝕜] at ha;
  simpa using hs.smul_mono ha

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

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

Разделы

Аффилиация

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