irrational_sub_ratCast_iff — Mathlib

English

Let q be a rational number and x a real number. Then x − q is irrational if and only if x is irrational.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem irrational_sub_ratCast_iff : Irrational (x - q) ↔ Irrational x :=
  ⟨of_sub_ratCast q, sub_ratCast q⟩

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