Finset.sup_singleton

Stream: Is there code for X?

[Jireh Loreaux]

Surely we have this? Loogle is failing me.

import Mathlib

example {α : Type*} (s : Finset α) : ⨆ x ∈ s, {x}  = s := sorry

[Jireh Loreaux]

nevermind, I think I'm looking in the wrong direction.

[Yaël Dillies]

It exists but not quite as stated

[Jireh Loreaux]

It's okay, I didn't end up needing it.

[Yaël Dillies]

It will be stated using Finset.biUnion. Lucky dip: docs#Finset.biUnion_singleton