instCanonicallyOrderedAdd — Mathlib

English

PartENat is a canonically ordered additive structure; addition is compatible with the natural order.

Русский

PartENat образует канонически упорядоченную аддитивную структуру; сложение совместимо с порядком.

LaTeX

$$$ \text{CanonicallyOrderedAdd}(\mathrm{PartENat})$$$

Lean4

instance : CanonicallyOrderedAdd PartENat
    where
  le_self_add a
    b :=
    PartENat.casesOn b (le_top.trans_eq (add_top _).symm) fun _ =>
      PartENat.casesOn a (top_add _).ge fun _ => (coe_le_coe.2 le_self_add).trans_eq (Nat.cast_add _ _)
  le_add_self a
    b :=
    PartENat.casesOn b (le_top.trans_eq (top_add _).symm) fun _ =>
      PartENat.casesOn a (add_top _).ge fun _ => (coe_le_coe.2 le_add_self).trans_eq (Nat.cast_add _ _)
  exists_add_of_le
    {a
      b} :=
    PartENat.casesOn b (fun _ => ⟨⊤, (add_top _).symm⟩) fun b =>
      PartENat.casesOn a (fun h => ((natCast_lt_top _).not_ge h).elim) fun a h =>
        ⟨(b - a : ℕ), by rw [← Nat.cast_add, natCast_inj, add_comm, tsub_add_cancel_of_le (coe_le_coe.1 h)]⟩

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