ordinal_type_le — Mathlib

English

If there is a rel-embedding from r into s, then type(r) ≤ type(s).

Русский

Если существует вложение отношения из r в s, то type(r) ≤ type(s).

LaTeX

$$$(\exists h: r \hookrightarrow r\ s)\Rightarrow \operatorname{type}(r) \le \operatorname{type}(s).$$$

Lean4

theorem _root_.RelEmbedding.ordinal_type_le {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r]
    [IsWellOrder β s] (h : r ↪r s) : type r ≤ type s :=
  ⟨h.collapse⟩

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