ssubset lemma

Stream: new members

[Matt Diamond]

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]

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]

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]

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]

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

[Yaël Dillies]

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