lt_ord_of_lt — Mathlib

English

If l < l' in product order and all ordinals of l are less than o, then all ordinals of l' are less than o.

Русский

Если l < l' в произведении упорядочения и для всех i∈l.val ord(i) < o, тогда то же верно и для l'.

LaTeX

$$$\\forall i\\in l.val\\;\\forall j\\in m.val\\; (\\mathrm{ord}_I(i) < o)$$$

Lean4

theorem lt_ord_of_lt {l m : Products I} {o : Ordinal} (h₁ : m < l) (h₂ : ∀ i ∈ l.val, ord I i < o) :
    ∀ i ∈ m.val, ord I i < o :=
  List.Sorted.lt_ord_of_lt (List.isChain_iff_pairwise.mp l.2) (List.isChain_iff_pairwise.mp m.2) h₁ h₂

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