search

metamath / set.mm

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

iset.mm: two theorems related to equinumerosity of real numbers #4066

Closed jkingdon closed 3 months ago

jkingdon commented 3 months ago

Although this is some distance from #4042 it seems like proving a few theorems about equinumerosity of real number intervals is a good first step.

This includes:

  1. two closed intervals are equinumerous
  2. an open interval is equinumerous to the reals
  3. updating an author name