smulAntidiagonal_mono_left — Mathlib

English

If u ⊆ s, then SMulAntidiagonal on u is contained in SMulAntidiagonal on s.

Русский

Если u ⊆ s, то SMulAntidiagonal на u вложено в SMulAntidiagonal на s.

LaTeX

$$SMulAntidiagonal hu ht a ⊆ SMulAntidiagonal hs ht a$$

Lean4

@[to_additive]
theorem smulAntidiagonal_mono_left {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : u ⊆ s) :
    SMulAntidiagonal hu ht a ⊆ SMulAntidiagonal hs ht a :=
  Set.Finite.toFinset_mono <| Set.smulAntidiagonal_mono_left h

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