Theorems · Theorem · combinatorics

Finset.support_vaddAntidiagonal_subset_vadd

∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P}
  (hst : ∀ (a : P), (s.vaddAntidiagonal t a).Finite), {a | (Finset.VAddAntidiagonal a ⋯).Nonempty} ⊆ s +ᵥ t

Defined in

Mathlib.Data.Finset.SMulAntidiagonal

Cited by

3 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

VAdd