const_lt

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.const_lt

English

const x < const y iff x < y.

Русский

const x < const y эквивалентно x < y.

LaTeX

$$$\bigl(\mathrm{const}\, x \lt \mathrm{const}\, y\bigr) \iff x < y.$$$

Lean4

theorem const_lt {x y : α} : const x < const y ↔ x < y :=
  show Pos _ ↔ _ by rw [← const_sub, const_pos, sub_pos]

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

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

Разделы

Аффилиация

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