Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_eq

Modification history

2021-10-31 01:33

src/logic/basic.lean

chore(logic/embedding): docs, fixes (#10047) …

Modified exists_eq View on Github →

2018-06-02 10:36

logic/basic.lean

feat(computability/turing_machine): proving the TM reductions

Modified exists_eq View on Github →

2017-09-03 20:55

logic/basic.lean

refactor(logic/basic): refactor logic theorems

Added exists_eq View on Github →