of_sub_ratCast — Mathlib

English

Let q be a rational number and x a real number. If x − q is irrational, then x is irrational.

Русский

Пусть q ∈ ℚ и x ∈ ℝ. Если x − q иррационально, то x иррационально.

LaTeX

$$$$\forall q \in \mathbb{Q}, \forall x \in \mathbb{R}, \operatorname{Irrational}(x - q) \\Rightarrow \operatorname{Irrational}(x).$$$$

Lean4

theorem of_sub_ratCast (h : Irrational (x - q)) : Irrational x :=
  of_add_ratCast (-q) <| by simpa only [cast_neg, sub_eq_add_neg] using h

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