feat(data/finset/lattice): add sup_image (#7428)

This also renames `finset.map_sup` to `finset.sup_map` to match `finset.sup_insert` and `finset.sup_singleton`.

The `inf` versions are added too.

Author: eric-wieser

src/data/finset/fold.lean

@@ -71,6 +71,16 @@ begin
   { apply fold_insert h },
 end
 
+theorem fold_image_idem [decidable_eq α] {g : γ → α} {s : finset γ}
+  [hi : is_idempotent β op] :
+  (image g s).fold op b f = s.fold op b (f ∘ g) :=
+begin
+  induction s using finset.cons_induction with x xs hx ih,
+  { rw [fold_empty, image_empty, fold_empty] },
+  { haveI := classical.dec_eq γ,
+    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih], }
+end
+
 lemma fold_op_rel_iff_and
   {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ (r x y ∧ r x z)) {c : β} :
   r c (s.fold op b f) ↔ (r c b ∧ ∀ x∈s, r c (f x)) :=

src/data/finset/lattice.lean

@@ -37,6 +37,14 @@ fold_cons h
 @[simp] lemma sup_insert [decidable_eq β] {b : β} : (insert b s : finset β).sup f = f b ⊔ s.sup f :=
 fold_insert_idem
 
+lemma sup_image [decidable_eq β] (s : finset γ) (f : γ → β) (g : β → α):
+  (s.image f).sup g = s.sup (g ∘ f) :=
+fold_image_idem
+
+@[simp] lemma sup_map (s : finset γ) (f : γ ↪ β) (g : β → α) :
+  (s.map f).sup g = s.sup (g ∘ f) :=
+fold_map
+
 @[simp] lemma sup_singleton {b : β} : ({b} : finset β).sup f = f b :=
 sup_singleton
 
@@ -63,10 +71,6 @@ sup_le_iff.2
 lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f :=
 sup_le_iff.1 (le_refl _) _ hb
 
-@[simp] lemma map_sup (f : γ ↪ β) (g : β → α) (s : finset γ) :
-  (s.map f).sup g = s.sup (g ∘ f) :=
-by simp [finset.sup]
-
 lemma sup_mono_fun {g : β → α} (h : ∀b∈s, f b ≤ g b) : s.sup f ≤ s.sup g :=
 sup_le (λ b hb, le_trans (h b hb) (le_sup hb))
 
@@ -180,6 +184,14 @@ fold_empty
 @[simp] lemma inf_insert [decidable_eq β] {b : β} : (insert b s : finset β).inf f = f b ⊓ s.inf f :=
 fold_insert_idem
 
+lemma inf_image [decidable_eq β] (s : finset γ) (f : γ → β) (g : β → α):
+  (s.image f).inf g = s.inf (g ∘ f) :=
+fold_image_idem
+
+@[simp] lemma inf_map (s : finset γ) (f : γ ↪ β) (g : β → α) :
+  (s.map f).inf g = s.inf (g ∘ f) :=
+fold_map
+
 @[simp] lemma inf_singleton {b : β} : ({b} : finset β).inf f = f b :=
 inf_singleton
 
@@ -198,10 +210,6 @@ le_inf_iff.1 (le_refl _) _ hb
 lemma le_inf {a : α} : (∀b ∈ s, a ≤ f b) → a ≤ s.inf f :=
 le_inf_iff.2
 
-@[simp] lemma map_inf (f : γ ↪ β) (g : β → α) (s : finset γ) :
-  (s.map f).inf g = s.inf (g ∘ f) :=
-by simp [finset.inf]
-
 lemma inf_mono_fun {g : β → α} (h : ∀b∈s, f b ≤ g b) : s.inf f ≤ s.inf g :=
 le_inf (λ b hb, le_trans (inf_le hb) (h b hb))