of_sub_intCast

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Irrational.of_sub_intCast

English

If x is irrational and m is an integer, then x − m.cast is irrational.

Русский

Если x иррационально и m — целое число, то x − m иррационально.

LaTeX

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

Lean4

theorem of_sub_intCast (m : ℤ) (h : Irrational (x - m)) : Irrational x :=
  of_sub_ratCast m <| by rwa [Rat.cast_intCast]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru