cast_le_intCast

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#Rat.cast_le_intCast

English

The inequality (m : K) ≤ n with n ∈ ℤ is equivalent to m ≤ n in ℚ.

Русский

Неравенство (m : K) ≤ n, где n ∈ ℤ, эквивалентно m ≤ n в ℚ.

LaTeX

$$$ \forall {m : \mathbb{Q}} {n : \mathbb{Z}}, \ (m : K) \le n \leftrightarrow m \le (n : \mathbb{Q}). $$$

Lean4

@[simp, norm_cast]
theorem cast_le_intCast {m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by rw [← cast_le (K := K), cast_intCast]

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

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

Разделы

Аффилиация

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