English
Let a be an element of the nonnegative part of an ordered semifield α, and b be any element of α. Then the natural embedding of b into the nonnegative part preserves the order, i.e. a < the embedded b if and only if the underlying α-value of a is less than b.
Русский
Пусть a принадлежит неотрицательной части поля с линейным порядком α, а b — произвольный элемент α. Тогда естественная вложение b в неотрицательную часть сохраняет порядок: a < встроенный b тогда и только тогда, когда собственно a < b.
LaTeX
$$$a < \\iota(b) \\iff a_{\\alpha} < b$, где $a \\in \\{x \\in \\alpha : 0 \\le x\\}$ и $b \\in \\alpha$$$
Lean4
@[simp]
theorem toNonneg_lt {a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b :=
by
obtain ⟨a, ha⟩ := a
simp [toNonneg, ha.not_gt]
