support_mulAntidiagonal_subset_mul

English

The set of all a for which mulAntidiagonal hs ht a is nonempty is contained in s·t.

Русский

Множество всех a, для которых mulAntidiagonal hs ht a непусто, содержится в s·t.

LaTeX

$${a | (mulAntidiagonal hs ht a).Nonempty} ⊆ s t$$

Lean4

@[to_additive]
theorem support_mulAntidiagonal_subset_mul : {a | (mulAntidiagonal hs ht a).Nonempty} ⊆ s * t := fun a ⟨b, hb⟩ =>
  by
  rw [mem_mulAntidiagonal] at hb
  exact ⟨b.1, hb.1, b.2, hb.2⟩

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