mem_balancedHull_iff — Mathlib

English

An element x lies in the balanced hull of s iff there exists a scalar r with norm at most 1 such that x ∈ r•s.

Русский

Элемент x принадлежит сбалансированной оболочке s тогда и только тогда, когда существует скаляр r с нормой не более 1, такой что x ∈ r•s.

LaTeX

$$$x \\in balancedHull\\ 𝕜\\ s \\iff \\exists r:\\\\ 𝕜, \\|r\\| \\le 1 \\land x \\in r\\cdot s$$$

Lean4

theorem mem_balancedHull_iff : x ∈ balancedHull 𝕜 s ↔ ∃ r : 𝕜, ‖r‖ ≤ 1 ∧ x ∈ r • s := by simp [balancedHull]

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