instAddRightMono — Mathlib

English

Right addition is order-preserving: if a ≤ b, then a + c ≤ b + c.

Русский

Правая сумма сохраняет порядок: если a ≤ b, то a + c ≤ b + c.

LaTeX

$$$ a \le b \Rightarrow a + c \le b + c $$$

Lean4

instance instAddRightMono : AddRightMono Ordinal.{u} where
  elim c a
    b :=
    by
    refine
      inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
        (RelEmbedding.ofMonotone (Sum.recOn · (Sum.inl ∘ f) Sum.inr) ?_).ordinal_type_le
    simp [f.map_rel_iff]

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