instAddLeftReflectLE — Mathlib

English

Left addition preserves the order: if a ≤ b then a + c ≤ b + c for all c.

Русский

Слева прибавление сохраняет порядок: если a ≤ b, то a + c ≤ b + c для любого c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ a \le b \Rightarrow a+c \le b+c$$$

Lean4

instance instAddLeftReflectLE : AddLeftReflectLE Ordinal.{u} where
  elim c a
    b := by
    refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦ ?_
    have H₁ a : f (Sum.inl a) = Sum.inl a := by simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a
    have H₂ a : ∃ b, f (Sum.inr a) = Sum.inr b :=
      by
      generalize hx : f (Sum.inr a) = x
      obtain x | x := x
      · rw [← H₁, f.inj] at hx
        contradiction
      · exact ⟨x, rfl⟩
    choose g hg using H₂
    refine (RelEmbedding.ofMonotone g fun _ _ h ↦ ?_).ordinal_type_le
    rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]

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