-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(data/option/basic): lemmas on map of none and congr #5424
Conversation
pechersky
commented
Dec 18, 2020
@@ -106,6 +106,18 @@ by cases x; simp | |||
x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := | |||
by cases x; simp | |||
|
|||
lemma map_eq_none {α β} {x : option α} {f : α → β} : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lemma map_eq_none {α β} {x : option α} {f : α → β} : | |
@[simp] lemma map_eq_none {α β} {x : option α} {f : α → β} : |
like below? Or is there a reason not to?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
simp linter complains if both are simp
afair.
by { cases x; simp only [map_none', map_some', eq_self_iff_true] } | ||
|
||
lemma map_congr {f g : α → β} {x : option α} (h : ∀ a ∈ x, f a = g a) : | ||
option.map f x = option.map g x := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this lemma would be better if you left it without the x
in the result (and maybe also the hypothesis. If you do that, then you can claim that map
is injective
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How would you phrase the hypothesis then? I've found this lemma useful for the cases when x
is some complex expression, and f a = g a
for all some a
for that complex x
, but not in the general case.
There's already an option.map_injective
lemma.
LGTM. bors merge |
Pull request successfully merged into master. Build succeeded: |