Mathlib v3 is deprecated. Go to Mathlib v4

Theorem option.injective_some

Modification history

2020-06-18 22:26

src/data/option/basic.lean

chore(*): regularize naming using injective (#3071) …

Deleted option.injective_some View on Github →

2018-09-05 11:53

data/option.lean

feat(logic/embedding): embedding into option

Added option.injective_some View on Github →