## Stream: Is there code for X?

### Topic: Insert lemmas

#### 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).

#### Eric Wieser (Oct 01 2020 at 17:41):

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

#### Jason KY. (Oct 01 2020 at 17:42):

That works great! Thanks

Last updated: May 07 2021 at 23:11 UTC