ofLower_lt_ofLower — Mathlib

English

Let α be a preorder. Then the map ofLower : WithLower α → α is an order-embedding; equivalently, for all x,y ∈ WithLower α, x < y iff ofLower x < ofLower y.

Русский

Пусть α — предпорядок. Тогда отображение ofLower : WithLower α → α является вложением по порядку; эквивалентно: для любых x,y ∈ WithLower α верно x < y тогда и только тогда, когда ofLower x < ofLower y.

LaTeX

$$$\\forall x,y : \\mathrm{WithLower} \\; \\alpha,\\ \\operatorname{ofLower} x < \\operatorname{ofLower} y \\iff x < y$$$

Lean4

@[simp]
theorem ofLower_lt_ofLower {x y : WithLower α} : ofLower x < ofLower y ↔ x < y :=
  .rfl

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