add_nat_iff — Mathlib

English

For all p, x real and all natural n, LiouvilleWith p (x + n) is equivalent to LiouvilleWith p x.

Русский

Для всех p, x вещественных и натурального n выполняется LiouvilleWith p (x + n) эквивалентно LiouvilleWith p x.

LaTeX

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

Lean4

@[simp]
theorem add_nat_iff : LiouvilleWith p (x + n) ↔ LiouvilleWith p x := by rw [← Rat.cast_natCast n, add_rat_iff]

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