Set.mem_setOf_eq

Stream: mathlib4

[Adam Topaz]

Is the name of docs4#Set.mem_setOf_eq actually correct?

[Yaël Dillies]

Looks correct to me. How else would you name it?

[Anne Baanen]

Didn't we replace all the _eq lemmas with _iff lemmas anyway?

[Ruben Van de Velde]

{ x | p x } is called setOf, I think

[Yaël Dillies]

Not this one :frowning:

[Adam Topaz]

oh okay it's fine. I thought it was a lemma of the form $x \in S$ implies $x \in T$ when $S = T$.

[Adam Topaz]

I should look at the type more carefully next time :)