Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.Icc.one_sub_nonneg

Modification history

2022-08-18 13:46

src/data/set/intervals/instances.lean

feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712) …

Added set.Icc.one_sub_nonneg View on Github →