cast_le

Mathlib.Data.Rat.Cast.Order

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

English

The cast preserves inequalities: (p : K) ≤ q iff p ≤ q.

Русский

Приведение сохраняет неравенство: (p : K) ≤ q эквивалентно p ≤ q.

LaTeX

$$$ \forall {p,q : \mathrm{Rat}} [..], \ (p : K) \le q \leftrightarrow p \le q. $$$

Lean4

@[simp, norm_cast]
theorem cast_le : (p : K) ≤ q ↔ p ≤ q :=
  castOrderEmbedding.le_iff_le

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

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

Разделы

Аффилиация

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