# Adjoining a zero/one to semigroups and mapping #

source
def WithOne.map {α : Type u_1} {β : Type u_2} (f : α → β) :
WithOne α → WithOne β

Lift a map `f : α → β` to `WithOne α → WithOne β`. Implemented using `Option.map`.

Note: the definition previously known as `WithOne.map` is now called `WithOne.mapMulHom`.

Equations

- WithOne.map f = Option.map f

Instances For

source
def WithZero.map {α : Type u_1} {β : Type u_2} (f : α → β) :
WithZero α → WithZero β

Lift a map `f : α → β` to `WithZero α → WithZero β`. Implemented using `Option.map`.

Note: the definition previously known as `WithZero.map` is now called `WithZero.mapAddHom`.

Equations

- WithZero.map f = Option.map f

Instances For

source
@[simp]
theorem WithOne.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) :
map f 1 = 1
source
@[simp]
theorem WithZero.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) :
map f 0 = 0
source
@[simp]
theorem WithOne.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
map f ↑a = ↑(f a)
source
@[simp]
theorem WithZero.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
map f ↑a = ↑(f a)
source
def WithOne.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α → β → γ) → WithOne α → WithOne β → WithOne γ

The image of a binary function `f : α → β → γ` as a function `WithOne α → WithOne β → WithOne γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.

Equations

- WithOne.map₂ = Option.map₂

Instances For

source
def WithZero.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α → β → γ) → WithZero α → WithZero β → WithZero γ

The image of a binary function `f : α → β → γ` as a function `WithZero α → WithZero β → WithZero γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.

Equations

- WithZero.map₂ = Option.map₂

Instances For

source
theorem WithOne.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) :
map₂ f ↑a ↑b = ↑(f a b)
source
theorem WithZero.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) :
map₂ f ↑a ↑b = ↑(f a b)
source
@[simp]
theorem WithOne.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithOne β) :
map₂ f 1 b = 1
source
@[simp]
theorem WithZero.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithZero β) :
map₂ f 0 b = 0
source
@[simp]
theorem WithOne.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithOne α) :
map₂ f a 1 = 1
source
@[simp]
theorem WithZero.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithZero α) :
map₂ f a 0 = 0
source
@[simp]
theorem WithOne.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithOne β) :
map₂ f (↑a) b = map (fun (b : β) => f a b) b
source
@[simp]
theorem WithZero.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithZero β) :
map₂ f (↑a) b = map (fun (b : β) => f a b) b
source
@[simp]
theorem WithOne.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithOne α) (b : β) :
map₂ f a ↑b = map (fun (x : α) => f x b) a
source
@[simp]
theorem WithZero.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithZero α) (b : β) :
map₂ f a ↑b = map (fun (x : α) => f x b) a
source
@[simp]
theorem WithOne.map₂_eq_bot_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithOne α} {b : WithOne β} :
map₂ f a b = 1 ↔ a = 1 ∨ b = 1
source
@[simp]
theorem WithZero.map₂_eq_bot_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithZero α} {b : WithZero β} :
map₂ f a b = 0 ↔ a = 0 ∨ b = 0