rat_add_iff — Mathlib

English

For any p, x real and any rational r, LiouvilleWith p (r + x) is equivalent to LiouvilleWith p x.

Русский

Для любых p, x вещественных и рационального r, LiouvilleWith p (r + x) эквивалентно LiouvilleWith p x.

LaTeX

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

Lean4

@[simp]
theorem rat_add_iff : LiouvilleWith p (r + x) ↔ LiouvilleWith p x := by rw [add_comm, add_rat_iff]

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