Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.range_inclusion

Modification history

2022-12-07 20:30
src/data/set/basic.lean
refactor(data/set/basic): move image, preimage, and range to a new file (#17842) …
Modified set.range_inclusionView on Github →
2022-04-29 12:25
src/data/set/basic.lean
feat(group_theory/subgroup/basic): `inclusion` lemmas (#13754) …
Modified set.range_inclusionView on Github →
2021-02-01 03:11
src/data/set/basic.lean
chore(*): golf some proofs (#5983) …
Modified set.range_inclusionView on Github →
2020-02-22 16:24
src/data/set/basic.lean
feat(*): misc simple lemmas (#2036) …
Added set.range_inclusionView on Github →