of_ratCast_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_ratCast_sub (h : Irrational (q - x)) : Irrational x :=
  of_neg (of_ratCast_add q (by simpa only [sub_eq_add_neg] using h))

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