mulAntidiagonal_mono_left — Mathlib

English

If U ⊆ S, then mulAntidiagonal with U is contained in mulAntidiagonal with S (on the left factor).

Русский

Если U ⊆ S, то mulAntidiagonal на левой части монотонно растет: mulAntidiagonal(u) ⊆ mulAntidiagonal(s).

LaTeX

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

Lean4

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

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