egauge_le_one — Mathlib

English

Let s be a subset of a normed space E. If x belongs to s, then the extended gauge of x with respect to s is at most 1, i.e., egauge 𝕜 s x ≤ 1.

Русский

Пусть s ⊆ E. Если x ∈ s, то расширенная шкала (egauge) точки x по отношению к s не превосходит 1: egauge 𝕜 s x ≤ 1.

LaTeX

$$$\\forall 𝕜\\,[\\text{NormedField } 𝕜],\\;\\forall s\\subseteq E,\\;\\forall x\\in s: \\operatorname{egauge}_{\\mathbb{k}}(s,x) \\le 1.$$$

Lean4

theorem egauge_le_one (h : x ∈ s) : egauge 𝕜 s x ≤ 1 :=
  by
  rw [← one_smul 𝕜 s] at h
  simpa using egauge_le_of_mem_smul h

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