Adjoining top/bottom elements to ordered monoids. #
@[simp]
@[simp]
Equations
- ⋯ = ⋯
Equations
- WithTop.add = { add := Option.map₂ fun (x x_1 : α) => x + x_1 }
instance
WithTop.covariantClass_swap_add_le
{α : Type u}
[Add α]
[LE α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
CovariantClass (WithTop α) (WithTop α) (Function.swap fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) =>
x ≤ x_1
Equations
- ⋯ = ⋯
instance
WithTop.contravariantClass_swap_add_lt
{α : Type u}
[Add α]
[LT α]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
:
ContravariantClass (WithTop α) (WithTop α) (Function.swap fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) =>
x < x_1
Equations
- ⋯ = ⋯
theorem
WithTop.add_le_add_iff_left
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
[LE α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(ha : a ≠ ⊤)
:
theorem
WithTop.add_le_add_iff_right
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
[LE α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(ha : a ≠ ⊤)
:
theorem
WithTop.add_lt_add_iff_left
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
[LT α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(ha : a ≠ ⊤)
:
theorem
WithTop.add_lt_add_iff_right
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
[LT α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(ha : a ≠ ⊤)
:
theorem
WithTop.add_lt_add_of_le_of_lt
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
{d : WithTop α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(ha : a ≠ ⊤)
(hab : a ≤ b)
(hcd : c < d)
:
theorem
WithTop.add_lt_add_of_lt_of_le
{α : Type u}
[Add α]
{a : WithTop α}
{b : WithTop α}
{c : WithTop α}
{d : WithTop α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(hc : c ≠ ⊤)
(hab : a < b)
(hcd : c ≤ d)
:
@[simp]
theorem
WithTop.map_add
{α : Type u}
{β : Type v}
[Add α]
{F : Type u_1}
[Add β]
[FunLike F α β]
[AddHomClass F α β]
(f : F)
(a : WithTop α)
(b : WithTop α)
:
WithTop.map (⇑f) (a + b) = WithTop.map (⇑f) a + WithTop.map (⇑f) b
Equations
- WithTop.addSemigroup = let __src := WithTop.add; AddSemigroup.mk ⋯
Equations
- WithTop.addCommSemigroup = let __src := WithTop.addSemigroup; AddCommSemigroup.mk ⋯
Equations
- WithTop.addZeroClass = let __src := WithTop.zero; let __src_1 := WithTop.add; AddZeroClass.mk ⋯ ⋯
Coercion from α
to WithTop α
as an AddMonoidHom
.
Equations
- WithTop.addHom = { toFun := WithTop.some, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- WithTop.addCommMonoid = let __src := WithTop.addMonoid; let __src_1 := WithTop.addCommSemigroup; AddCommMonoid.mk ⋯
Equations
- WithTop.addMonoidWithOne = let __src := WithTop.one; let __src_1 := WithTop.addMonoid; AddMonoidWithOne.mk ⋯ ⋯
@[deprecated WithTop.coe_natCast]
Alias of WithTop.coe_natCast
.
@[deprecated WithTop.natCast_ne_top]
Alias of WithTop.natCast_ne_top
.
@[deprecated WithTop.top_ne_natCast]
Alias of WithTop.top_ne_natCast
.
@[simp]
theorem
WithTop.coe_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
↑(OfNat.ofNat n) = OfNat.ofNat n
@[simp]
theorem
WithTop.coe_eq_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
(m : α)
:
↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
@[simp]
theorem
WithTop.ofNat_eq_coe
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
(m : α)
:
OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
@[simp]
theorem
WithTop.ofNat_ne_top
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
OfNat.ofNat n ≠ ⊤
@[simp]
theorem
WithTop.top_ne_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
⊤ ≠ OfNat.ofNat n
Equations
- ⋯ = ⋯
Equations
- WithTop.addCommMonoidWithOne = let __src := WithTop.addMonoidWithOne; let __src_1 := WithTop.addCommMonoid; AddCommMonoidWithOne.mk ⋯
instance
WithTop.existsAddOfLE
{α : Type u}
[LE α]
[Add α]
[ExistsAddOfLE α]
:
ExistsAddOfLE (WithTop α)
Equations
- ⋯ = ⋯
theorem
ZeroHom.withTopMap.proof_1
{M : Type u_2}
{N : Type u_1}
[Zero M]
[Zero N]
(f : ZeroHom M N)
:
WithTop.map (⇑f) 0 = 0
A version of WithTop.map
for ZeroHom
s
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯ }
Instances For
@[simp]
theorem
OneHom.withTopMap_apply
{M : Type u_1}
{N : Type u_2}
[One M]
[One N]
(f : OneHom M N)
:
⇑f.withTopMap = WithTop.map ⇑f
@[simp]
theorem
ZeroHom.withTopMap_apply
{M : Type u_1}
{N : Type u_2}
[Zero M]
[Zero N]
(f : ZeroHom M N)
:
⇑f.withTopMap = WithTop.map ⇑f
A version of WithTop.map
for OneHom
s.
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, map_one' := ⋯ }
Instances For
@[simp]
theorem
AddHom.withTopMap_apply
{M : Type u_1}
{N : Type u_2}
[Add M]
[Add N]
(f : AddHom M N)
:
⇑f.withTopMap = WithTop.map ⇑f
A version of WithTop.map
for AddHom
s.
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, map_add' := ⋯ }
Instances For
@[simp]
theorem
AddMonoidHom.withTopMap_apply
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
:
⇑f.withTopMap = WithTop.map ⇑f
def
AddMonoidHom.withTopMap
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
:
A version of WithTop.map
for AddMonoidHom
s.
Equations
- f.withTopMap = let __src := (↑f).withTopMap; let __src := (↑f).withTopMap; { toFun := WithTop.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
@[simp]
Equations
- ⋯ = ⋯
Equations
- WithBot.AddSemigroup = WithTop.addSemigroup
Equations
- WithBot.addCommSemigroup = WithTop.addCommSemigroup
Equations
- WithBot.addZeroClass = WithTop.addZeroClass
Coercion from α
to WithBot α
as an AddMonoidHom
.
Equations
- WithBot.addHom = { toFun := WithTop.some, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- WithBot.addCommMonoid = WithTop.addCommMonoid
Equations
- WithBot.addMonoidWithOne = WithTop.addMonoidWithOne
@[deprecated WithBot.coe_natCast]
Alias of WithBot.coe_natCast
.
@[deprecated WithBot.natCast_ne_bot]
Alias of WithBot.natCast_ne_bot
.
@[deprecated WithBot.bot_ne_natCast]
Alias of WithBot.bot_ne_natCast
.
@[simp]
theorem
WithBot.coe_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
↑(OfNat.ofNat n) = OfNat.ofNat n
@[simp]
theorem
WithBot.coe_eq_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
(m : α)
:
↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
@[simp]
theorem
WithBot.ofNat_eq_coe
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
(m : α)
:
OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
@[simp]
theorem
WithBot.ofNat_ne_bot
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
OfNat.ofNat n ≠ ⊥
@[simp]
theorem
WithBot.bot_ne_ofNat
{α : Type u}
[AddMonoidWithOne α]
(n : ℕ)
[n.AtLeastTwo]
:
⊥ ≠ OfNat.ofNat n
Equations
- ⋯ = ⋯
Equations
- WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne
@[simp]
theorem
WithBot.map_add
{α : Type u}
{β : Type v}
[Add α]
{F : Type u_1}
[Add β]
[FunLike F α β]
[AddHomClass F α β]
(f : F)
(a : WithBot α)
(b : WithBot α)
:
WithBot.map (⇑f) (a + b) = WithBot.map (⇑f) a + WithBot.map (⇑f) b
A version of WithBot.map
for ZeroHom
s
Equations
- f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯ }
Instances For
theorem
ZeroHom.withBotMap.proof_1
{M : Type u_2}
{N : Type u_1}
[Zero M]
[Zero N]
(f : ZeroHom M N)
:
WithBot.map (⇑f) 0 = 0
@[simp]
theorem
OneHom.withBotMap_apply
{M : Type u_1}
{N : Type u_2}
[One M]
[One N]
(f : OneHom M N)
:
⇑f.withBotMap = WithBot.map ⇑f
@[simp]
theorem
ZeroHom.withBotMap_apply
{M : Type u_1}
{N : Type u_2}
[Zero M]
[Zero N]
(f : ZeroHom M N)
:
⇑f.withBotMap = WithBot.map ⇑f
A version of WithBot.map
for OneHom
s.
Equations
- f.withBotMap = { toFun := WithBot.map ⇑f, map_one' := ⋯ }
Instances For
@[simp]
theorem
AddHom.withBotMap_apply
{M : Type u_1}
{N : Type u_2}
[Add M]
[Add N]
(f : AddHom M N)
:
⇑f.withBotMap = WithBot.map ⇑f
A version of WithBot.map
for AddHom
s.
Equations
- f.withBotMap = { toFun := WithBot.map ⇑f, map_add' := ⋯ }
Instances For
@[simp]
theorem
AddMonoidHom.withBotMap_apply
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
:
⇑f.withBotMap = WithBot.map ⇑f
def
AddMonoidHom.withBotMap
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
:
A version of WithBot.map
for AddMonoidHom
s.
Equations
- f.withBotMap = let __src := (↑f).withBotMap; let __src := (↑f).withBotMap; { toFun := WithBot.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
instance
WithBot.covariantClass_swap_add_le
{α : Type u}
[Add α]
[Preorder α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
CovariantClass (WithBot α) (WithBot α) (Function.swap fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) =>
x ≤ x_1
Equations
- ⋯ = ⋯
instance
WithBot.contravariantClass_swap_add_lt
{α : Type u}
[Add α]
[Preorder α]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
:
ContravariantClass (WithBot α) (WithBot α) (Function.swap fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) =>
x < x_1
Equations
- ⋯ = ⋯
theorem
WithBot.add_le_add_iff_left
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(ha : a ≠ ⊥)
:
theorem
WithBot.add_le_add_iff_right
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
[Preorder α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(ha : a ≠ ⊥)
:
theorem
WithBot.add_lt_add_iff_left
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(ha : a ≠ ⊥)
:
theorem
WithBot.add_lt_add_iff_right
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
[Preorder α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(ha : a ≠ ⊥)
:
theorem
WithBot.add_lt_add_of_le_of_lt
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
{d : WithBot α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
(hb : b ≠ ⊥)
(hab : a ≤ b)
(hcd : c < d)
:
theorem
WithBot.add_lt_add_of_lt_of_le
{α : Type u}
[Add α]
{a : WithBot α}
{b : WithBot α}
{c : WithBot α}
{d : WithBot α}
[Preorder α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(hd : d ≠ ⊥)
(hab : a < b)
(hcd : c ≤ d)
: