lsub_sum — Mathlib

English

For f: Sum α β → Ordinal, lsub f equals the maximum of lsub over the left part and the right part, i.e., lsub f = max(lsub f∘inl, lsub f∘inr).

Русский

Для функции f: (α ⊕ β) → Ordinal имеем lsub f = max(lsub f∘inl, lsub f∘inr).

LaTeX

$$$\operatorname{lsub} f = \max\Big( \operatorname{lsub}(\lambda a. f(\mathrm{Sum}.inl a)), \operatorname{lsub}(\lambda b. f(\mathrm{Sum}.inr b)) \Big)$$$

Lean4

@[simp]
theorem lsub_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal) :
    lsub.{max u v, w} f = max (lsub.{u, max v w} fun a => f (Sum.inl a)) (lsub.{v, max u w} fun b => f (Sum.inr b)) :=
  iSup_sum _

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