## Stream: Is there code for X?

### Topic: finset.erase_singleton_self

#### Kenny Lau (May 23 2020 at 07:43):

import data.finset

universe u

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
sorry


#### Scott Morrison (May 23 2020 at 08:38):

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
begin
ext y,
split,
{ intro h,
simp at h,
contradiction, },
{ rintro ⟨⟩, }
end


it seems it should go in the library, as a @[simp] lemma

#### Bryan Gin-ge Chen (May 23 2020 at 09:06):

I'm surprised it's not already there!

#### Mario Carneiro (May 23 2020 at 09:20):

probably the move from insert to singleton was a factor

#### Bhavik Mehta (May 23 2020 at 12:03):

Not at a computer right now but I think there should be an easier proof using insert_eq and erase_insert?

#### Bhavik Mehta (May 23 2020 at 13:18):

open finset

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
by rw [← insert_emptyc_eq, erase_insert (not_mem_empty x)]


????

#### Kenny Lau (May 23 2020 at 13:24):

https://github.com/leanprover-community/lean/blob/970d47ce28b1637375a76f490339baffa165fc2c/library/init/core.lean#L404-L409

class is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β]
[has_singleton α β] :=
(insert_emptyc_eq : ∀ (x : α), (insert x ∅ : β) = {x})

export has_singleton (singleton)
export is_lawful_singleton (insert_emptyc_eq)


#### Kenny Lau (May 23 2020 at 13:24):

those damn exports

Last updated: May 07 2021 at 19:12 UTC