cast_le

Mathlib.Algebra.Order.Ring.Cast

URI: https://scilib.ai/kg/mathlib#Int.cast_le

English

Cast preserves order: m.cast ≤ n.cast iff m ≤ n.

Русский

Приведение сохраняет порядок: m.cast ≤ n.cast если и только если m ≤ n.

LaTeX

$$$m^{\mathsf{cast}} \le n^{\mathsf{cast}} \;\iff\; m \le n$$$

Lean4

@[simp, norm_cast]
theorem cast_le : (m : R) ≤ n ↔ m ≤ n := by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]

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

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

Разделы

Аффилиация

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