Adjoining a zero/one to semigroups and mapping

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.

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.

@[simp]

theorem WithOne.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) : map f 1 = 1

@[simp]

theorem WithZero.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) : map f 0 = 0

@[simp]

theorem WithOne.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f ↑a = ↑(f a)

@[simp]

theorem WithZero.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f ↑a = ↑(f a)

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 α × β → γ.

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 α × β → γ.

theorem WithOne.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f ↑a ↑b = ↑(f a b)

theorem WithZero.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f ↑a ↑b = ↑(f a b)

@[simp]

theorem WithOne.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithOne β) : map₂ f 1 b = 1

@[simp]

theorem WithZero.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithZero β) : map₂ f 0 b = 0

@[simp]

theorem WithOne.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithOne α) : map₂ f a 1 = 1

@[simp]

theorem WithZero.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithZero α) : map₂ f a 0 = 0

@[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

@[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

@[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

@[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

@[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

@[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