Theorems · Theorem · combinatorics

Finset.HasAntidiagonal.filter_fst_eq_antidiagonal

∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A] [inst_3 : Sub A]
  [OrderedSub A] [AddLeftReflectLE A] [inst_6 : Finset.HasAntidiagonal A] (n m : A)
  [inst_7 : DecidablePred fun x => x = m] [inst_8 : Decidable (m ≤ n)],
  {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅

Defined in

Mathlib.Algebra.Order.Antidiag.Prod

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderCanonicallyOrderedAddSubOrderedSubAddLeftReflectLEFinset.HasAntidiagonalDecidablePredDecidable