add_int_iff — Mathlib

English

For all p, x real and all integers m, LiouvilleWith p (x + m) is equivalent to LiouvilleWith p x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add_int_iff : LiouvilleWith p (x + m) ↔ LiouvilleWith p x := by rw [← Rat.cast_intCast m, add_rat_iff]

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