search

metamath / set.mm

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

Add apdiff to iset.mm mathbox #3998

Closed jkingdon closed 3 months ago

jkingdon commented 3 months ago

This is a way of characterizing irrationals as exactly those reals that are a different distance from every rational:

    apdiff $p |- ( A e. RR -> ( A. q e. QQ A =//= q <-> A. q e. QQ A. r e. QQ
        ( q =/= r -> ( abs ` ( A - q ) ) =//= ( abs ` ( A - r ) ) ) ) ) $=
jkingdon commented 3 months ago

NIce! Would it make sense to have a set.mm version?

I'm working on one. Might be another few days as my idea is to make a more streamlined proof than is possible in iset.mm.

jkingdon commented 3 months ago

Oh I should also mention the post where I saw this theorem stated: https://mathstodon.xyz/@ColinTheMathmo/112455490217662534

tirix commented 3 months ago

Might be another few days as my idea is to make a more streamlined proof than is possible in iset.mm.

Can we merge this first?

jkingdon commented 3 months ago

Might be another few days as my idea is to make a more streamlined proof than is possible in iset.mm.

Can we merge this first?

Merging this one now sounds good to me.