type_sum_lex — Mathlib

English

The type of the lexicographic sum of two well-orders equals the sum of their types.

Русский

Тип лексикографической суммы двух хорошо упорядоченных множеств равен сумме их типов.

LaTeX

$$$ \operatorname{type}(\mathrm{Sum.Lex}(r,s)) = \operatorname{type}(r) + \operatorname{type}(s) $$$

Lean4

@[simp]
theorem type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] :
    type (Sum.Lex r s) = type r + type s :=
  rfl

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