mulAntidiagonal_mono_left — Mathlib

English

If s1 is contained in s2, then mulAntidiagonal s1 t a is contained in mulAntidiagonal s2 t a.

Русский

Если s1 ⊆ s2, то mulAntidiagonal(s1, t, a) ⊆ mulAntidiagonal(s2, t, a).

LaTeX

$$$s_1 \subseteq s_2 \implies mulAntidiagonal\,(s_1,t,a) \subseteq mulAntidiagonal\,(s_2,t,a)$.$$

Lean4

@[to_additive]
theorem mulAntidiagonal_mono_left (h : s₁ ⊆ s₂) : mulAntidiagonal s₁ t a ⊆ mulAntidiagonal s₂ t a := fun _ hx =>
  ⟨h hx.1, hx.2.1, hx.2.2⟩

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