add_rat_iff — Mathlib

English

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

Русский

Для всех p, x вещественных и для каждого рационального r LiouvilleWith p (x + r) эквивалентно 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 add_rat_iff : LiouvilleWith p (x + r) ↔ LiouvilleWith p x :=
  ⟨fun h => by simpa using h.add_rat (-r), fun h => h.add_rat r⟩

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