neg — Mathlib

English

If h is LiouvilleWith p x, then LiouvilleWith p (-x) holds.

Русский

Если h имеет LiouvilleWith p x, то LiouvilleWith p (-x) верно.

LaTeX

$$$LiouvilleWith(p, x) \to LiouvilleWith(p, -x)$$$

Lean4

protected theorem neg (h : LiouvilleWith p x) : LiouvilleWith p (-x) :=
  by
  rcases h with ⟨C, hC⟩
  refine ⟨C, hC.mono ?_⟩
  rintro n ⟨m, hne, hlt⟩
  refine ⟨-m, by simp [neg_div, hne], ?_⟩
  convert hlt using 1
  rw [abs_sub_comm]
  congr! 1; push_cast; ring

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