Zulip Chat Archive

Stream: Is there code for X?

Topic: Insert lemmas


view this post on Zulip Jason KY. (Oct 01 2020 at 17:31):

Do we have these two insert lemmas?

lemma set.insert_inter_of_mem {s₁ s₂ : set α} {a : α} (h : a  s₂) :
  insert a s₁  s₂ = insert a (s₁  s₂) :=
by { ext, split; finish }

lemma set.insert_inter_of_not_mem {s₁ s₂ : set α} {a : α} (h : a  s₂) :
  insert a s₁  s₂ = s₁  s₂ :=
by { ext, split; finish }

I think they are pretty useful but I can't seem to find them anywhere (I was able to find a finset version but not for set).

view this post on Zulip Eric Wieser (Oct 01 2020 at 17:41):

docs#set.insert_inter followed by docs#set.insert_eq_of_mem?

view this post on Zulip Jason KY. (Oct 01 2020 at 17:42):

That works great! Thanks


Last updated: May 07 2021 at 23:11 UTC