partialOrder — Mathlib

English

The localization Localization(s) of a commutative cancellative monoid carries a natural partial order, extending the original order and made compatible with multiplication. In particular, the order is defined by the representatives of fractions and yields a well-defined partial order on Localization(s).

Русский

У локализации Localization(s) коммутативного отменимого моноида имеется естественный частичный порядок, расширяющий исходный порядок и совместимый с умножением. Порядок задаётся через представления долей и образует корректный частичный порядок на Localization(s).

LaTeX

$$$\\operatorname{PartialOrder}(\\operatorname{Localization}(s))$$$

Lean4

@[to_additive]
instance partialOrder : PartialOrder (Localization s)
    where
  le := (· ≤ ·)
  lt := (· < ·)
  le_refl a := Localization.induction_on a fun _ => le_rfl
  le_trans a b
    c :=
    Localization.induction_on₃ a b c fun a b c hab hbc =>
      by
      simp only [mk_le_mk] at hab hbc ⊢
      apply le_of_mul_le_mul_left' _
      · exact ↑b.2
      rw [mul_left_comm]
      refine (mul_le_mul_left' hab _).trans ?_
      rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]
  le_antisymm a
    b := by
    induction a using Localization.rec
    on_goal 1 =>
      induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
    all_goals rfl
  lt_iff_le_not_ge a b := Localization.induction_on₂ a b fun _ _ => lt_iff_le_not_ge

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