smul — Mathlib

English

If s and t have well-founded order with respect to the product structure, then their product s • t also has IsPWO.

Русский

Если множества s и t образуют хорошо упорядоченную пару в произведении, то их произведение s • t также обладает свойством IsPWO.

LaTeX

$$IsPWO(s) → IsPWO(t) → IsPWO(s • t)$$

Lean4

@[to_additive]
theorem smul [Preorder G] [Preorder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO)
    (ht : t.IsPWO) : IsPWO (s • t) := by
  rw [← @image_smul_prod]
  exact (hs.prod ht).image_of_monotone (monotone_fst.smul monotone_snd)

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