seminormFromBounded_neg — Mathlib

English

If f is invariant under x ↦ −x, then seminormFromBounded' f is also invariant under negation.

Русский

Если f инвариантна относительно замены x на −x, то seminormFromBounded' f также инвариантна по отрицанию.

LaTeX

$$$\operatorname{seminormFromBounded}' f(-x) = \operatorname{seminormFromBounded}' f(x)$$$

Lean4

/-- If `f` is invariant under negation of `x`, then so is `seminormFromBounded'`. -/
theorem seminormFromBounded_neg (f_neg : ∀ x : R, f (-x) = f x) (x : R) :
    seminormFromBounded' f (-x) = seminormFromBounded' f x :=
  by
  suffices ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y by simpa only [seminormFromBounded']
  congr
  ext y
  rw [neg_mul, f_neg]

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