smul — Mathlib

English

If s and t are IsWF sets under given linear orders and scalar action, then s • t is IsWF.

Русский

Если s и t имеют свойство IsWF относительно данных линейных порядков и скалярного умножения, то s • t тоже IsWF.

LaTeX

$$IsWF(s) → IsWF(t) → IsWF(s • t)$$

Lean4

@[to_additive]
theorem smul [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF)
    (ht : t.IsWF) : IsWF (s • t) :=
  (hs.isPWO.smul ht.isPWO).isWF

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