gauge_neg — Mathlib

English

Gauge is invariant under negation with a symmetric set: gauge s (−x) = gauge s (x).

Русский

Gauge инвариантна относительно отрицания при симметричном s: gauge s (−x) = gauge s (x).

LaTeX

$$$$\\operatorname{gauge}(s, -x) = \\operatorname{gauge}(s, x). $$$$

Lean4

theorem gauge_neg (symmetric : ∀ x ∈ s, -x ∈ s) (x : E) : gauge s (-x) = gauge s x :=
  by
  have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩
  simp_rw [gauge_def', smul_neg, this]

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