irrational_intCast_sub_iff — Mathlib

English

Let m be an integer and x a real number. Then m − x is irrational if and only if x is irrational.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem irrational_intCast_sub_iff : Irrational (m - x) ↔ Irrational x :=
  ⟨of_intCast_sub m, fun h => h.intCast_sub m⟩

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