Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.exists

Modification history

2021-01-03 02:24
src/data/prod.lean
chore(data/prod): add `prod.forall'` and `prod.exists'` (#5570) …
Deleted prod.existsView on Github →
2017-12-06 13:30
data/prod.lean
feature(.): add various theorems
Modified prod.existsView on Github →
2017-09-03 20:55
logic/basic.lean
refactor(logic/basic): refactor logic theorems
Modified prod.existsView on Github →
2017-07-23 18:59
logic/basic.lean
refactor(*): attributes on same line
Modified prod.existsView on Github →
2017-07-23 18:29
logic/basic.lean
refactor(*): use 'lemma' iff statement is private
Modified prod.existsView on Github →
2017-07-23 15:16
logic/basic.lean
refactor(*): import content from lean/library/data and library_dev
Added prod.existsView on Github →