support_smulAntidiagonal_subset_smul

English

The sigma of s and t is nonempty iff there exists i ∈ s with t(i) nonempty.

Русский

Сигма-объединение s и t непусто тогда и только тогда, когда существует i ∈ s такое, что t(i) непусто.

LaTeX

$$$ (s.sigma t).Nonempty \iff \Exists i \in s, (t i).Nonempty $$$

Lean4

@[to_additive]
theorem support_smulAntidiagonal_subset_smul {hs : s.IsPWO} {ht : t.IsPWO} :
    {a | (SMulAntidiagonal hs ht a).Nonempty} ⊆ (s • t) := fun a ⟨b, hb⟩ =>
  by
  rw [mem_smulAntidiagonal] at hb
  rw [Set.mem_smul]
  use b.1
  refine { left := hb.1, right := ?_ }
  use b.2
  exact { left := hb.2.1, right := hb.2.2 }

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