neg_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

URI: https://scilib.ai/kg/mathlib#LiouvilleWith.neg_iff

English

LiouvilleWith p (-x) is equivalent to LiouvilleWith p x.

Русский

LiouvilleWith p (-x) эквивалентно LiouvilleWith p x.

LaTeX

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

Lean4

@[simp]
theorem neg_iff : LiouvilleWith p (-x) ↔ LiouvilleWith p x :=
  ⟨fun h => neg_neg x ▸ h.neg, LiouvilleWith.neg⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru