Theorems · Theorem · combinatorics

Set.SMulAntidiagonal.finite_of_isPWO

∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : SMul G P] [IsOrderedCancelSMul G P], s.IsPWO → t.IsPWO → ∀ (a : P), (s.smulAntidiagonal t a).Finite

Defined in

Mathlib.Data.Set.SMulAntidiagonal

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderPartialOrderSMulIsOrderedCancelSMul