theorem Set.sep_setOftheorem Set.sep_setOf: { x ∈ { y | p y } | q x } = { x | p x ∧ q x }
Published by @sam · Jul 21, 2026
View source in zpg9xh52
zpg9xh52
Definitional, with no premises to accept.
Set.sep_setOf
definitional fact