imageProdLex — Mathlib

English

If s is PWOn in the ProdLex order, then the image of s under the fst-projection is PWOn in α.

Русский

Если s частично хорошо упорядочено по ProdLex, тогда образ s по проекции на первый фактор является PWOn в α.

LaTeX

$$s.IsPWO \rightarrow ((fun x => (fst x)) '' s).IsPWO$$

Lean4

theorem imageProdLex [Preorder α] [Preorder β] {s : Set (α ×ₗ β)} (hαβ : s.IsPWO) :
    ((fun (x : α ×ₗ β) => (ofLex x).1) '' s).IsPWO :=
  IsPWO.image_of_monotone hαβ Prod.Lex.monotone_fst

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