Zulip Chat Archive

Stream: new members

Topic: ssubset lemma

Matt Diamond (Aug 06 2022 at 03:36):

Is there a lemma in mathlib like the following?

lemma sdiff_singleton_ssubset {α : Type*} {a : set α} {x : α} (h: x  a) : a \ {x}  a := sorry

Something like docs#set.ssubset_insert, but with removal instead of addition. I know about docs#finset.sdiff_ssubset, but that's for finsets and not exactly the same.

I realize it's not difficult to prove, but I'm just surprised it doesn't exist already (or doesn't seem to) and was wondering if I was overlooking something.

Alex J. Best (Aug 06 2022 at 03:46):

I don't think you've missed anything, it seems there is docs#finset.sdiff_ssubset, which would be what I'd want to use to prove your lemma but its only for finsets, so probably a couple of missing lemmas here!

Alex J. Best (Aug 06 2022 at 03:50):

Actually there is docs#sdiff_lt for boolean algebras, so one proof is as follows

lemma sdiff_singleton_ssubset {α : Type*} {a : set α} {x : α} (h: x  a) : a \ {x}  a := sdiff_lt (show {x}  a, from set.singleton_subset_iff.mpr h) (set.singleton_nonempty _).ne_empty

this probably still should be a lemma for sets

Yaël Dillies (Aug 06 2022 at 06:20):

One of the many lemmas I have lying on a branch... (or in that case #10865 I believe). Feel free to PR it because I won't have time for another week.

Ruben Van de Velde (Aug 06 2022 at 07:11):

What's blocking #10865? Just a merge with master and a review?

Yaël Dillies (Aug 06 2022 at 07:12):

It should prove the more general statement about docs#covby.

Last updated: Dec 20 2023 at 11:08 UTC