mulAntidiagonal_mono_right — Mathlib

English

If U ⊆ T, then mulAntidiagonal with U on the right is contained in mulAntidiagonal with T on the right.

Русский

Если U ⊆ T, то mulAntidiagonal с правой стороны монотонно растет: mulAntidiagonal(s, u) ⊆ mulAntidiagonal(s, t).

LaTeX

$$If u ⊆ t, then mulAntidiagonal hs hu a ⊆ mulAntidiagonal hs ht a$$

Lean4

@[to_additive]
theorem mulAntidiagonal_mono_right (h : u ⊆ t) : mulAntidiagonal hs hu a ⊆ mulAntidiagonal hs ht a :=
  Set.Finite.toFinset_mono <| Set.mulAntidiagonal_mono_right h

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