nat_sub — Mathlib

English

If x satisfies a Liouville condition with exponent p, then for every natural number n the shifted number n − x also satisfies the same Liouville condition with the same exponent p.

Русский

Если число x удовлетворяет условию Лиувилля с показателем p, то для любого натурального числа n число n − x также удовлетворяет этому условию Лиувиля с тем же показателем p.

LaTeX

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

Lean4

theorem nat_sub (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (n - x) :=
  nat_sub_iff.2 h

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