const_lt_iff — Mathlib

English

The order on constant germs matches the base order: (↑x) < (↑y) in Germ β iff x < y in β.

Русский

Порядок на константных Гермах совпадает с порядком в β: (↑x) < (↑y) в Germ β эквивалентно x < y в β.

LaTeX

$$$(\\uparrow x) < (\\uparrow y) \\iff x < y.$$$

Lean4

@[simp, norm_cast]
theorem const_lt_iff [Preorder β] {x y : β} : (↑x : β*) < ↑y ↔ x < y :=
  coe_lt.trans liftRel_const_iff

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