Fix typo in definition of projections in beta-function lemma.

OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook

http://openlogicproject.org/

Creative Commons Attribution 4.0 International

1.04k stars 237 forks source link

Closed beastaugh closed 2 years ago

beastaugh commented 2 years ago

The minimization is now bounded by the input pair z rather than some free q.

The second commit just fixes an incorrect reference to a proposition used in the proof of Lindenbaum's lemma.