rat_sub_iff — Mathlib

English

Translation by a rational number preserves LiouvilleWith: LiouvilleWith p (r − x) ⇔ LiouvilleWith p x for any rational r.

Русский

Сдвиг на рациональный число сохраняет свойство Лиувиля: LiouvilleWith p (r − x) ⇔ LiouvilleWith p x для любого рационального r.

LaTeX

$$$\\forall p,x \\in \\mathbb{R},\\forall r \\in \\mathbb{Q},\\ LiouvilleWith(p, r - x) \\iff LiouvilleWith(p, x).$$$

Lean4

@[simp]
theorem rat_sub_iff : LiouvilleWith p (r - x) ↔ LiouvilleWith p x := by simp [sub_eq_add_neg]

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