mulRightMono — Mathlib

English

For every fixed ordinal c, the map a ↦ a · c is monotone in a; i.e., if a ≤ b then a · c ≤ b · c.

Русский

Для фиксированного порядкового числа c отображение a ↦ a · c монотонно по a; то есть если a ≤ b, то a · c ≤ b · c.

LaTeX

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

Lean4

instance mulRightMono : MulRightMono Ordinal.{u} :=
  ⟨fun c a b =>
    Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩ =>
      by
      refine (RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => ?_).ordinal_type_le
      obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
      · exact Prod.Lex.left _ _ h'
      · exact Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')⟩

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