Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Expected behavior of partition

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Expected behavior of partition


Chronological Thread 
  • From: Florent Hivert <>
  • To: BEGAY Pierre-leo <>
  • Subject: Re: [ssreflect] Expected behavior of partition
  • Date: Mon, 16 Dec 2019 16:51:04 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:k30fIBZfkGpg2zjy+zYCbVL/LSx+4OfEezUN459isYplN5qZoMq9bnLW6fgltlLVR4KTs6sC17ON9fq4BCdQuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6txvdutUWjIdtKas91wbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFKH4GyYJYVD+cZM+hWr5fzqUYNoxuwCgajGP7gxT1GiXLtwa02z/gtHR3a0AE6Ad4DtmnfotXvNKcVVOC41KnGzTHEb/NMxzj97pTIeQ0jr/GNQ7J/b9DRyVUyHA7CjluQrYvlPymL2eQLr2iX9ehuVeOxi2E5sQFxviOixsM2ionInI4VxErE+Dx/zY0oJtO4UFZ2bcO6HJZUrS2WKol7T8M4T211uCs20KAKtYK9cSMX0poo3QTfZOaCc4WQ4hLsSuKRITBgiXJgYr2/hhKy/lavy+3gTMW01ExKritfntnCrHABzx3T6s6ZRfth5kqtxCiD2gTJ5u1ZI005lbDXJ4Mhz7Iqi5YfrVzPHirsl0X3iK+WeF8k+u+t6+n/YrvmopicN5VqhQH4LqQigM6xAeUmMgcQRWib5f+x1Ln5/U34WrlKgOc2nrHDsJ/GPcQburK5AwhN34Y48Ba/FSmp0NocnXYZMF1FZAmKj5PpOlHLOPD3F+2zg1WqkDdxxvDJJKftApvXLiuLrLC0V5tSwn8U8As+18pSopZZDflVOPj+VUbgnNHeFVoyOge0yuChBs8rha0EXmfaLKueKq7UrReo5/wiOfXEMKERvyzwLeRjx//wgGUlsVsHfO+nx81EOziDAv16LhDBMjLXidAbHDJP51JmFb24uBi5STdWIk2Kcec57zA/BpihCNeRQpqsxrKbjn7iQ89mI1teA1XJKk/GMoWJX/BVNnCXK85lnywYE7y7Sskvz0P27VOo+/9cNuPRvxYgm9f7ztEltenJlFc8724sAg==
  • Resent-date: Mon, 16 Dec 2019 16:53:41 +0100
  • Resent-from: Florent Hivert <>
  • Resent-message-id: <>
  • Resent-to: "" <>
Dear Pierre-leo,

On Mon, Dec 16, 2019 at 04:12:05PM +0100, BEGAY Pierre-leo wrote:
> and I think that multiple occurrences of a set in P are not captured by the
> sum. This can be sort of checked with the following lemma, that - as far as
> I understand the usual definition of a set partition - should be false:

There can't be multiple occurrences of an element in a set, ie duplicates are
removed automatically by definition.

> (* setT can be partitioned into two copies of itself *)
> Lemma partitionF {A : finType} (wit : A) : partition [set [set: A]; setT]

In your case, [set: A] and setT design the same set. Actually

Lemma bla {A : finType} : [set: A] = setT.
Proof. by []. Qed.

So that [set [set: A]; setT] = [set [set: A]].

Lemma blo {A : finType} : [set [set: A]; setT] = [set [set: A]].
Proof.
apply/eqP; rewrite eqEsubset;apply/andP.
by split;apply/subsetP => x; rewrite !inE orbb.
Qed.

It is a perfectly valid partition.

Best,

Florent

Archive powered by MHonArc 2.6.18.

Top of Page