search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

decidability of real number equality implies WLPO #4041

Closed jkingdon closed 3 months ago

jkingdon commented 3 months ago

Or in the notation of #4040 , A. x e. RR A. y e. RR DECID x = y -> _om e. Womni

This theorem is taken from "Analytic WLPO" at https://ncatlab.org/nlab/show/principle+of+omniscience#analytic