Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 05:50 82fd6e1e

View on Github →

feat(logic/girard): Girard's paradox (#7026) A proof of Girard's paradox in lean, based on the LF proof: http://www.cs.cmu.edu/~kw/research/hurkens95tlca.elf

Estimated changes

Modified src/logic/basic.lean

added theorem cast_eq_iff_heq

Created src/logic/girard.lean

added theorem {u}

Modified src/logic/small.lean

added theorem not_small_type

added theorem small_type