Mathlib v3 is deprecated. Go to Mathlib v4

Theorem classical.or_not

Modification history

2020-08-17 13:59
src/logic/basic.lean
refactor(logic/basic): classical -> root, root -> decidable (#3812) …
Deleted classical.or_notView on Github →
2017-11-23 23:33
logic/basic.lean
feat(data/finset): fintype, multiset.sort, list.pmap
Modified classical.or_notView on Github →
2017-09-28 18:08
logic/basic.lean
feat(topology): add Lebesgue measure
Modified classical.or_notView on Github →
2017-09-21 13:22
topology/outer_measure.lean
feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable
Added classical.or_notView on Github →
2017-09-21 10:33
topology/outer_measure.lean
Merge branch 'master' of https://github.com/leanprover/mathlib
Deleted classical.or_notView on Github →
2017-09-20 20:02
topology/outer_measure.lean
feat(topology/outer_measure): add outer measures and tools for Caratheodorys extension method
Added classical.or_notView on Github →