ordinal_type_le — Mathlib

English

If h is an initial segment embedding from r into s, then the order-type of r is less than or equal to the order-type of s.

Русский

Если h является вложением начального сегмента из r в s, то порядок-тип r не превосходит порядок-тип s.

LaTeX

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

Lean4

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

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