coe_lt_coe

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.coe_lt_coe

English

Coercion preserves strict order: (p : ℚ) < q iff p < q.

Русский

Приведение сохраняет строгий порядок: (p : ℚ) < q iff p < q.

LaTeX

$$$$ (p : \mathbb{Q}) < q \iff p < q. $$$$

Lean4

@[norm_cast]
theorem coe_lt_coe : (p : ℚ) < q ↔ p < q :=
  Iff.rfl

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

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

Разделы

Аффилиация

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