Zulip Chat Archive

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:22):

Kenny Lau (May 23 2020 at 13:22):

????

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: Dec 20 2023 at 11:08 UTC