smulAntidiagonal_mono_right — Mathlib

English

If v ⊆ t, then SMulAntidiagonal on v is contained in SMulAntidiagonal on t.

Русский

Если v ⊆ t, то SMulAntidiagonal на v вложено в SMulAntidiagonal на t.

LaTeX

$$SMulAntidiagonal hs hv a ⊆ SMulAntidiagonal hs ht a$$

Lean4

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

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