theorem WithBot.map_add' {α : Type u_1} {β : Type u_2} {f : α → β} (a b : WithBot α) [Add α] [Add β] (hf : ∀ (x y : α), f (x + y) = f x + f y) : map f (a + b) = map f a + map f b

theorem WithTop.map_add' {α : Type u_1} {β : Type u_2} {f : α → β} (a b : WithTop α) [Add α] [Add β] (hf : ∀ (x y : α), f (x + y) = f x + f y) : map f (a + b) = map f a + map f b

theorem WithBot.map_lt_iff {α : Type u_1} {β : Type u_2} (a b : WithBot α) [LT α] [LT β] (f : α → β) (mono_iff : ∀ {a b : α}, f a < f b ↔ a < b) : map f a < map f b ↔ a < b

theorem WithTop.map_lt_iff {α : Type u_1} {β : Type u_2} (a b : WithTop α) [LT α] [LT β] (f : α → β) (mono_iff : ∀ {a b : α}, f b < f a ↔ b < a) : map f b < map f a ↔ b < a