English
The relation on the localization mk is determined by the cross-multiplication rule: mk a1 a2 ≤ mk b1 b2 iff b2 a1 ≤ a2 b1.
Русский
Отношение в локализации mk задаётся правилом переноса умножений: mk a1 a2 ≤ mk b1 b2 тогда и только тогда, когда b2 a1 ≤ a2 b1.
LaTeX
$$$mk\\, a_1 a_2 \\le mk\\, b_1 b_2 \\iff b_2 a_1 \\le a_2 b_1$$$
Lean4
@[to_additive]
instance le : LE (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_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α), mul_le_mul_iff_right,
← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm, mul_left_comm (b₂ : α), mul_le_mul_iff_left]⟩
