Zulip Chat Archive
Stream: new members
Topic: Well founded recursion with universes + universes and ord...
Fox Thomson (Aug 11 2020 at 11:46):
Managed to prove it by getting a contradiction from showing cardinal.univ.{u (u+1)} ≤ cardinal.lift.{u (u+1)} (cardinal.mk α), thank you!!
Last updated: Dec 20 2023 at 11:08 UTC