#constructivemathematics — Public Fediverse posts

The smallest positive real whose cosine is one is two times the smallest positive real whose sine is zero. Proved from axioms of IZF set theory via constructing reals, convergence and notation for infinite series, the exponential function, continuity, and the monotone intermediate value theorem. https://us.metamath.org/ileuni/taupi.html #PiDay #HalfTauDay #HalfTau #constructiveMathematics

@andrejbauer Although the style of the post I'm replying to befits its publication date, it has inspired me to prove the following https://github.com/metamath/set.mm/pull/3114 which complements existing similar proofs for ordinal trichotomy, regularity, the axiom of choice, the subset of a finite set being finite, and others. #constructiveMathematics #metamath

Oh and please boost the post at the top of this thread if you think people would be interested. I'm not sure how many math-interested people follow the #metamath or #constructiveMathematics tags.

I proved the ratio test for IZF in #metamath ! I knew this would be different in #constructiveMathematics because of the need to show how fast the series converges, but on the whole once I proved a basic convergence theorem based on a fixed rate of convergence, I have found that a lot of our convergence results work just like they did with excluded middle. (will put links in a reply to this message).

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics