isPWO_support_smulAntidiagonal — Mathlib

English

The set of a for which SMulAntidiagonal hs ht a is nonempty is contained in s • t.

Русский

Множество таких a, для которых SMulAntidiagonal hs ht a непусто, содержится в s • t.

LaTeX

$${a | (SMulAntidiagonal hs ht a).Nonempty} ⊆ (s • t)$$

Lean4

@[to_additive]
theorem isPWO_support_smulAntidiagonal {hs : s.IsPWO} {ht : t.IsPWO} :
    {a | (SMulAntidiagonal hs ht a).Nonempty}.IsPWO :=
  (hs.smul ht).mono (support_smulAntidiagonal_subset_smul)

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