feat(data/setoid/partition): Relate setoid.is_partition and `finpar…

…tition` (#12459)

Add two functions that relate `setoid.is_partition` and `finpartition`:
* `setoid.is_partition.partition` 
* `finpartition.is_partition_parts`
Meanwhile add some lemmas related to `finset.sup` and `finset.inf` in data/finset/lattice.


Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/finset/lattice.lean

@@ -249,6 +249,12 @@ le_antisymm
 lemma sup_id_eq_Sup [complete_lattice α] (s : finset α) : s.sup id = Sup s :=
 by simp [Sup_eq_supr, sup_eq_supr]
 
+lemma sup_id_set_eq_sUnion (s : finset (set α)) : s.sup id = ⋃₀(↑s) :=
+sup_id_eq_Sup _
+
+@[simp] lemma sup_set_eq_bUnion (s : finset α) (f : α → set β) : s.sup f = ⋃ x ∈ s, f x :=
+sup_eq_supr _ _
+
 lemma sup_eq_Sup_image [complete_lattice β] (s : finset α) (f : α → β) : s.sup f = Sup (f '' s) :=
 begin
   classical,
@@ -452,6 +458,12 @@ lemma inf_eq_infi [complete_lattice β] (s : finset α) (f : α → β) : s.inf
 lemma inf_id_eq_Inf [complete_lattice α] (s : finset α) : s.inf id = Inf s :=
 @sup_id_eq_Sup (order_dual α) _ _
 
+lemma inf_id_set_eq_sInter (s : finset (set α)) : s.inf id = ⋂₀(↑s) :=
+inf_id_eq_Inf _
+
+@[simp] lemma inf_set_eq_bInter (s : finset α) (f : α → set β) : s.inf f = ⋂ x ∈ s, f x :=
+inf_eq_infi _ _
+
 lemma inf_eq_Inf_image [complete_lattice β] (s : finset α) (f : α → β) : s.inf f = Inf (f '' s) :=
 @sup_eq_Sup_image _ (order_dual β) _ _ _
 

src/data/setoid/partition.lean

@@ -7,6 +7,7 @@ Authors: Amelia Livingston, Bryan Gin-ge Chen, Patrick Massot
 import data.fintype.basic
 import data.set.finite
 import data.setoid.basic
+import order.partition.finpartition
 
 /-!
 # Equivalence relations: partitions
@@ -20,9 +21,10 @@ There are two implementations of partitions here:
 
 Of course both implementations are related to `quotient` and `setoid`.
 
-## TODO
+`setoid.is_partition.partition` and `finpartition.is_partition_parts` furnish
+a link between `setoid.is_partition` and `finpartition`.
 
-Link `setoid.is_partition` and `finpartition`.
+## TODO
 
 Could the design of `finpartition` inform the one of `setoid.is_partition`? Maybe bundling it and
 changing it from `set (set α)` to `set α` where `[lattice α] [order_bot α]` would make it more
@@ -237,8 +239,23 @@ _ (subtype (@is_partition α)) _ (partial_order.to_preorder _) $ partition.order
 
 end partition
 
+/-- A finite setoid partition furnishes a finpartition -/
+@[simps]
+def is_partition.finpartition {c : finset (set α)}
+  (hc : setoid.is_partition (c : set (set α))) : finpartition (set.univ : set α) :=
+{ parts := c,
+  sup_indep := finset.sup_indep_iff_pairwise_disjoint.mpr $ eqv_classes_disjoint hc.2,
+  sup_parts := c.sup_id_set_eq_sUnion.trans hc.sUnion_eq_univ,
+  not_bot_mem := hc.left }
+
 end setoid
 
+/-- A finpartition gives rise to a setoid partition -/
+theorem finpartition.is_partition_parts {α} (f : finpartition (set.univ : set α)) :
+  setoid.is_partition (f.parts : set (set α)) :=
+⟨f.not_bot_mem, setoid.eqv_classes_of_disjoint_union
+  (f.parts.sup_id_set_eq_sUnion.symm.trans f.sup_parts) f.sup_indep.pairwise_disjoint⟩
+
 /-- Constructive information associated with a partition of a type `α` indexed by another type `ι`,
 `s : ι → set α`.
 

src/order/well_founded_set.lean

@@ -471,12 +471,10 @@ eq_of_mem_singleton (is_wf.min_mem hs hn)
 
 end set
 
-@[simp]
 theorem finset.is_wf_sup {ι : Type*} [partial_order α] (f : finset ι) (g : ι → set α)
   (hf : ∀ i : ι, i ∈ f → (g i).is_wf) : (f.sup g).is_wf :=
 finset.sup_induction set.is_pwo_empty.is_wf (λ a ha b hb, ha.union hb) hf
 
-@[simp]
 theorem finset.is_pwo_sup {ι : Type*} [partial_order α] (f : finset ι) (g : ι → set α)
   (hf : ∀ i : ι, i ∈ f → (g i).is_pwo) : (f.sup g).is_pwo :=
 finset.sup_induction set.is_pwo_empty (λ a ha b hb, ha.union hb) hf