source
theorem map_inj_of_left_inverse {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] {f : α → β} (w : ∃ (g : β → α), ∀ (x : α), g (f x) = x) {x y : m α} :
f <$> x = f <$> y ↔ x = y
source
@[simp]
theorem map_inj_right_of_nonempty {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β} (w : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
f <$> x = f <$> y ↔ x = y
source
@[simp]
theorem map_inj_right {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
f <$> x = f <$> y ↔ x = y