English
For linearly ordered cancellative semigroups, nonempty s,t satisfy #s + #t − 1 ≤ #(s t).
Русский
Для линейно упорядочённых отменяемых полугрупп непустые s,t удовлетворяют #s + #t − 1 ≤ #(s t).
LaTeX
$$$#s + #t - 1 \\le #(s * t)$.$$
Lean4
/-- The **Cauchy-Davenport Theorem** for linearly ordered cancellative semigroups. The size of
`s * t` is lower-bounded by `|s| + |t| - 1`. -/
@[to_additive /-- The **Cauchy-Davenport theorem** for linearly ordered additive cancellative semigroups. The
size of `s + t` is lower-bounded by `|s| + |t| - 1`. -/
]
theorem cauchy_davenport_mul_of_linearOrder_isCancelMul [LinearOrder α] [Mul α] [IsCancelMul α] [MulLeftMono α]
[MulRightMono α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : #s + #t - 1 ≤ #(s * t) :=
by
suffices s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
by
rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht), ← card_union_add_card_inter, ←
card_singleton _, ← this, Nat.add_sub_cancel]
exact
card_mono
(union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)
refine
eq_singleton_iff_unique_mem.2
⟨mem_inter.2
⟨mul_mem_mul (max'_mem _ _) <| mem_singleton_self _, mul_mem_mul (mem_singleton_self _) <| min'_mem _ _⟩,
?_⟩
simp only [mem_inter, and_imp, mem_mul, mem_singleton, exists_eq_left, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂, mul_left_inj]
exact fun a' ha' b' hb' h ↦
(le_max' _ _ ha').eq_of_not_lt fun ha ↦
((mul_lt_mul_right' ha _).trans_eq' h).not_ge <| mul_le_mul_left' (min'_le _ _ hb') _
