dedekind-reals icon indicating copy to clipboard operation
dedekind-reals copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Prove that the lift of negated disjunctions is enough to merge Cauchy…

Open VincentSe opened this issue 5 years ago • 1 comments

… and Dedekind reals

VincentSe avatar Aug 21 '19 22:08 VincentSe

Hi, sorry for not noticing this PR earlier. What do you mean by "merge" Cauchy and Dedekind reals? Which lemma in the PR expresses this?

andrejbauer avatar Dec 20 '23 08:12 andrejbauer