search

metamath / set.mm

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

Add irrdiff to set.mm #4002

Closed jkingdon closed 3 months ago

jkingdon commented 3 months ago

This is similar to apdiff from iset.mm but the theorem defines irrational differently and uses not equal in place of apart.

Includes lemma irrdifflemf .

See discussion at https://github.com/metamath/set.mm/pull/3998#pullrequestreview-2065479763

jkingdon commented 3 months ago

There's an informalization of this proof and a few more thoughts at https://sfba.social/@soaproot/112477489483787894 and the rest of that thread.