Theorems · Theorem · number theory

cauchy_davenport_add_of_linearOrder_isCancelAdd

∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : Add α] [IsCancelAdd α] [AddLeftMono α] [AddRightMono α]
  {s t : Finset α}, s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s + t).card

The Cauchy-Davenport theorem for linearly ordered additive cancellative semigroups. The size of s + t is lower-bounded by |s| + |t| - 1.

Defined in

Mathlib.Combinatorics.Additive.CauchyDavenport

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderAddIsCancelAddAddLeftMonoAddRightMono