English
There exists a natural strict order on the localization Local s that is defined by lifting to representatives; in particular, the order is compatible with the underlying monoid structure and is given by cross-multiplication of representatives.
Русский
Существует естественный строгий порядок на локализации Local s, задаваемый посредством перехода к представителям; порядок совместим с основным структуром моноида и задаётся через перекрёстное умножение представителем.
LaTeX
$$$ \\text{Localization}(s) \\text{ carries a canonical strict order defined by representatives and cross-multiplication.}$$$
Lean4
@[to_additive]
instance lt : LT (Localization s) :=
⟨fun a b =>
Localization.liftOn₂ a b (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < a₂ * b₁) fun {a₁ b₁ a₂ b₂ c₁ d₁ c₂ d₂} hab hcd =>
propext <| by
obtain ⟨e, he⟩ := r_iff_exists.1 hab
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
simp only [mul_right_inj] at he hf
dsimp
rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α), mul_lt_mul_iff_right,
← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm, mul_left_comm (b₂ : α), mul_lt_mul_iff_left]⟩
