Theorems · Theorem · combinatorics

Set.VAddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd

∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P] {x y : ↑(s.vaddAntidiagonal t a)},
  (↑x).1 ≤ (↑y).1 → (↑x).2 ≤ (↑y).2 → x = y

Defined in

Mathlib.Data.Set.SMulAntidiagonal

Cited by

1 results in Mathlib

Foundations

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

Assumes

PartialOrderPartialOrderVAddIsOrderedCancelVAdd