gauge_smul_left — Mathlib

English

If x ∈ s, then gauge s x ≤ 1 (same as gauge_le_one_of_mem).

Русский

Если x ∈ s, то gauge s x ≤ 1 (то же, что gauge_le_one_of_mem).

LaTeX

$$$$x \\in s \\Rightarrow \\mathrm{gauge}(s,x) \\le 1.$$$$

Lean4

theorem gauge_smul_left [Module α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ] [IsScalarTower α ℝ E] {s : Set E}
    (symmetric : ∀ x ∈ s, -x ∈ s) (a : α) : gauge (a • s) = |a|⁻¹ • gauge s :=
  by
  rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]
  obtain h | h := abs_choice a
  · rw [h]
  · rw [h, Set.neg_smul_set, ← Set.smul_set_neg]
    congr
    ext y
    refine ⟨symmetric _, fun hy => ?_⟩
    rw [← neg_neg y]
    exact symmetric _ hy

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