sub_int — Mathlib

English

If x is Liouville with respect to p, then x − m is Liouville with respect to p for every integer m.

Русский

Если x обладает свойством Лиувиля с параметром p, то x − m обладает тем же свойством для любого целого числа m.

LaTeX

$$$\\forall p \\in \\mathbb{R}, \\ \\forall x \\in \\mathbb{R},\\; LiouvilleWith(p,x) \\Rightarrow \\forall m \\in \\mathbb{Z},\\ LiouvilleWith(p, x - m).$$$

Lean4

theorem sub_int (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (x - m) :=
  sub_int_iff.2 h

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