finset.sup_attach

Stream: Is there code for X?

[Yaël Dillies]

Did I miss a generalization? Is there a slick proof of that?

import data.finset.lattice

lemma finset.sup_attach {α β : Type*} [semilattice_sup_bot α] (s : finset β) (f : β → α) :
  s.attach.sup (λ x, f x) = s.sup f :=
eq_of_forall_ge_iff $ λ c, begin
  rw [finset.sup_le_iff, finset.sup_le_iff],
  exact ⟨λ h b hb, h ⟨b, hb⟩ (s.mem_attach _), λ h b _, h b.1 b.2⟩,
end

[Yakov Pechersky]

import data.finset.lattice

lemma finset.sup_attach {α β : Type*} [semilattice_sup_bot α] (s : finset β) (f : β → α) :
  s.attach.sup (λ x, f x) = s.sup f :=
begin
  classical,
  induction s using finset.induction_on with x s hx IH generalizing f,
  { simp [finset.sup_image] },
  { simp only [finset.sup_image, finset.attach_insert, subtype.coe_mk, finset.sup_insert,
             subtype.val_eq_coe],
    rw ←IH,
    congr }
end

[Yakov Pechersky]

Oh sorry missed that you edited it

[Yaël Dillies]

Shorter :stuck_out_tongue:

[Yaël Dillies]

but I expect there's something more general about this "let's drop the proof" kind of thing.

[Eric Wieser]

Do we have docs#finset.sup_map or docs#finset.sup_image?

[Eric Wieser]

Yes; you can use that to pull the coercion out of the sup, and then you just need something like s.attach.map coe = s