coe_lt_coe

Mathlib.Order.Disjoint

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

English

The order is preserved for < as well.

Русский

Порядок < сохраняется под вложением.

LaTeX

$$$(a :\\alpha) < b \\iff a < b$$$

Lean4

@[norm_cast]
theorem coe_lt_coe : (a : α) < b ↔ a < b := by simp

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

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

Разделы

Аффилиация

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