Theorems · Theorem · combinatorics

Finset.smulAntidiagonal_mono_left

∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s u : Set G} {t : Set P} (a : P),
  u ⊆ s →
    ∀ (hst : (s.smulAntidiagonal t a).Finite) (hut : (u.smulAntidiagonal t a).Finite),
      Finset.SMulAntidiagonal a hut ⊆ Finset.SMulAntidiagonal a hst

Defined in: Mathlib.Data.Finset.SMulAntidiagonal
Cited by: 0 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement · cited by 13,712
Set.Finitestatement and proof · cited by 1,814
Set.smulAntidiagonalstatement and proof · cited by 17
Set.Finite.toFinset_monoproof · cited by 10
Finset.SMulAntidiagonalstatement · cited by 10
Set.smulAntidiagonal_mono_leftproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.