algebra.order.kleene - mathlib3 docs

source

@[instance]

def idem_semiring.to_semiring (α : Type u) [self : idem_semiring α] :

semiring α

source

@[class]

structure idem_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), idem_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), idem_semiring.nsmul n.succ x = x + idem_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : idem_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), idem_semiring.nat_cast (n + 1) = idem_semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), idem_semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), idem_semiring.npow n.succ x = x * idem_semiring.npow n x) . "try_refl_tac"
sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
add_eq_sup : (∀ (a b : α), a + b = a ⊔ b) . "try_refl_tac"
bot : α
bot_le : ∀ (a : α), idem_semiring.bot ≤ a

An idempotent semiring is a semiring with the additional property that addition is idempotent.

Instances of this typeclass

Instances of other typeclasses for idem_semiring

idem_semiring.has_sizeof_inst

source

@[instance]

def idem_semiring.to_semilattice_sup (α : Type u) [self : idem_semiring α] :

semilattice_sup α

source

@[instance]

def idem_comm_semiring.to_comm_semiring (α : Type u) [self : idem_comm_semiring α] :

comm_semiring α

source

@[instance]

def idem_comm_semiring.to_idem_semiring (α : Type u) [self : idem_comm_semiring α] :

idem_semiring α

source

@[class]

structure idem_comm_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), idem_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), idem_comm_semiring.nsmul n.succ x = x + idem_comm_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : idem_comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), idem_comm_semiring.nat_cast (n + 1) = idem_comm_semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), idem_comm_semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), idem_comm_semiring.npow n.succ x = x * idem_comm_semiring.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
add_eq_sup : (∀ (a b : α), a + b = a ⊔ b) . "try_refl_tac"
bot : α
bot_le : ∀ (a : α), idem_comm_semiring.bot ≤ a

An idempotent commutative semiring is a commutative semiring with the additional property that addition is idempotent.

Instances of this typeclass

Instances of other typeclasses for idem_comm_semiring

idem_comm_semiring.has_sizeof_inst

source

@[class]

structure has_kstar (α : Type u_5) :

Type u_5

kstar : α → α

Notation typeclass for the Kleene star ∗.

Instances of this typeclass

kleene_algebra.to_has_kstar

Instances of other typeclasses for has_kstar

has_kstar.has_sizeof_inst

source

@[instance]

def kleene_algebra.to_idem_semiring (α : Type u_5) [self : kleene_algebra α] :

idem_semiring α

source

@[class]

structure kleene_algebra (α : Type u_5) :

Type u_5

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), kleene_algebra.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), kleene_algebra.nsmul n.succ x = x + kleene_algebra.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : kleene_algebra.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), kleene_algebra.nat_cast (n + 1) = kleene_algebra.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), kleene_algebra.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), kleene_algebra.npow n.succ x = x * kleene_algebra.npow n x) . "try_refl_tac"
sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
add_eq_sup : (∀ (a b : α), a + b = a ⊔ b) . "try_refl_tac"
bot : α
bot_le : ∀ (a : α), kleene_algebra.bot ≤ a
kstar : α → α
one_le_kstar : ∀ (a : α), 1 ≤ has_kstar.kstar a
mul_kstar_le_kstar : ∀ (a : α), a * has_kstar.kstar a ≤ has_kstar.kstar a
kstar_mul_le_kstar : ∀ (a : α), has_kstar.kstar a * a ≤ has_kstar.kstar a
mul_kstar_le_self : ∀ (a b : α), b * a ≤ b → b * has_kstar.kstar a ≤ b
kstar_mul_le_self : ∀ (a b : α), a * b ≤ b → has_kstar.kstar a * b ≤ b

A Kleene Algebra is an idempotent semiring with an additional unary operator kstar (for Kleene star) that satisfies the following properties:

1 + a * a∗ ≤ a∗
1 + a∗ * a ≤ a∗
If a * c + b ≤ c, then a∗ * b ≤ c
If c * a + b ≤ c, then b * a∗ ≤ c

Instances of this typeclass

Instances of other typeclasses for kleene_algebra

kleene_algebra.has_sizeof_inst

source

@[instance]

def kleene_algebra.to_has_kstar (α : Type u_5) [self : kleene_algebra α] :

has_kstar α

source

@[protected, instance]

def idem_semiring.to_order_bot {α : Type u_1} [idem_semiring α] :

order_bot α

Equations

idem_semiring.to_order_bot = {bot := idem_semiring.bot _inst_1, bot_le := _}

source

@[reducible]

def idem_semiring.of_semiring {α : Type u_1} [semiring α] (h : ∀ (a : α), a + a = a) :

idem_semiring α

Construct an idempotent semiring from an idempotent addition.

Equations

idem_semiring.of_semiring h = {add := semiring.add _inst_1, add_assoc := _, zero := semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, sup := has_add.add (distrib.to_has_add α), le := λ (a b : α), a + b = b, lt := semilattice_sup.lt._default (λ (a b : α), a + b = b), le_refl := h, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := 0, bot_le := _}

source

@[simp]

theorem add_eq_sup {α : Type u_1} [idem_semiring α] (a b : α) :

a + b = a ⊔ b

source

theorem add_idem {α : Type u_1} [idem_semiring α] (a : α) :

a + a = a

source

theorem nsmul_eq_self {α : Type u_1} [idem_semiring α] {n : ℕ} (hn : n ≠ 0) (a : α) :

n • a = a

source

theorem add_eq_left_iff_le {α : Type u_1} [idem_semiring α] {a b : α} :

a + b = a ↔ b ≤ a

source

theorem add_eq_right_iff_le {α : Type u_1} [idem_semiring α] {a b : α} :

a + b = b ↔ a ≤ b

source

theorem has_le.le.add_eq_left {α : Type u_1} [idem_semiring α] {a b : α} :

b ≤ a → a + b = a

Alias of the reverse direction of add_eq_left_iff_le.

source

theorem has_le.le.add_eq_right {α : Type u_1} [idem_semiring α] {a b : α} :

a ≤ b → a + b = b

Alias of the reverse direction of add_eq_right_iff_le.

source

theorem add_le_iff {α : Type u_1} [idem_semiring α] {a b c : α} :

a + b ≤ c ↔ a ≤ c ∧ b ≤ c

source

theorem add_le {α : Type u_1} [idem_semiring α] {a b c : α} (ha : a ≤ c) (hb : b ≤ c) :

a + b ≤ c

source

@[protected, instance]

def idem_semiring.to_canonically_ordered_add_monoid {α : Type u_1} [idem_semiring α] :

canonically_ordered_add_monoid α

Equations

idem_semiring.to_canonically_ordered_add_monoid = {add := idem_semiring.add _inst_1, add_assoc := _, zero := idem_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := idem_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := idem_semiring.le _inst_1, lt := idem_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := idem_semiring.bot _inst_1, bot_le := _, exists_add_of_le := _, le_self_add := _}

source

@[protected, instance]

def idem_semiring.to_covariant_class_mul_le {α : Type u_1} [idem_semiring α] :

covariant_class α α has_mul.mul has_le.le

source

@[protected, instance]

def idem_semiring.to_covariant_class_swap_mul_le {α : Type u_1} [idem_semiring α] :

covariant_class α α (function.swap has_mul.mul) has_le.le

source

@[simp]

theorem one_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :

1 ≤ has_kstar.kstar a

source

theorem mul_kstar_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :

a * has_kstar.kstar a ≤ has_kstar.kstar a

source

theorem kstar_mul_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :

has_kstar.kstar a * a ≤ has_kstar.kstar a

source

theorem mul_kstar_le_self {α : Type u_1} [kleene_algebra α] {a b : α} :

b * a ≤ b → b * has_kstar.kstar a ≤ b

source

theorem kstar_mul_le_self {α : Type u_1} [kleene_algebra α] {a b : α} :

a * b ≤ b → has_kstar.kstar a * b ≤ b

source

theorem mul_kstar_le {α : Type u_1} [kleene_algebra α] {a b c : α} (hb : b ≤ c) (ha : c * a ≤ c) :

b * has_kstar.kstar a ≤ c

source

theorem kstar_mul_le {α : Type u_1} [kleene_algebra α] {a b c : α} (hb : b ≤ c) (ha : a * c ≤ c) :

has_kstar.kstar a * b ≤ c

source

theorem kstar_le_of_mul_le_left {α : Type u_1} [kleene_algebra α] {a b : α} (hb : 1 ≤ b) :

b * a ≤ b → has_kstar.kstar a ≤ b

source

theorem kstar_le_of_mul_le_right {α : Type u_1} [kleene_algebra α] {a b : α} (hb : 1 ≤ b) :

a * b ≤ b → has_kstar.kstar a ≤ b

source

@[simp]

theorem le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :

a ≤ has_kstar.kstar a

source

theorem kstar_mono {α : Type u_1} [kleene_algebra α] :

monotone has_kstar.kstar

source

@[simp]

theorem kstar_eq_one {α : Type u_1} [kleene_algebra α] {a : α} :

has_kstar.kstar a = 1 ↔ a ≤ 1

source

@[simp]

theorem kstar_zero {α : Type u_1} [kleene_algebra α] :

has_kstar.kstar 0 = 1

source

@[simp]

theorem kstar_one {α : Type u_1} [kleene_algebra α] :

has_kstar.kstar 1 = 1

source

@[simp]

theorem kstar_mul_kstar {α : Type u_1} [kleene_algebra α] (a : α) :

has_kstar.kstar a * has_kstar.kstar a = has_kstar.kstar a

source

@[simp]

theorem kstar_eq_self {α : Type u_1} [kleene_algebra α] {a : α} :

has_kstar.kstar a = a ↔ a * a = a ∧ 1 ≤ a

source

@[simp]

theorem kstar_idem {α : Type u_1} [kleene_algebra α] (a : α) :

has_kstar.kstar (has_kstar.kstar a) = has_kstar.kstar a

source

@[simp]

theorem pow_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} {n : ℕ} :

a ^ n ≤ has_kstar.kstar a

source

@[protected, instance]

def prod.idem_semiring {α : Type u_1} {β : Type u_2} [idem_semiring α] [idem_semiring β] :

idem_semiring (α × β)

Equations

prod.idem_semiring = {add := semiring.add prod.semiring, add_assoc := _, zero := semiring.zero prod.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul prod.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul prod.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast prod.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, sup := semilattice_sup.sup (prod.semilattice_sup α β), le := semilattice_sup.le (prod.semilattice_sup α β), lt := semilattice_sup.lt (prod.semilattice_sup α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := order_bot.bot (prod.order_bot α β), bot_le := _}

source

@[protected, instance]

def prod.idem_comm_semiring {α : Type u_1} {β : Type u_2} [idem_comm_semiring α] [idem_comm_semiring β] :

idem_comm_semiring (α × β)

Equations

prod.idem_comm_semiring = {add := comm_semiring.add prod.comm_semiring, add_assoc := _, zero := comm_semiring.zero prod.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul prod.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul prod.comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one prod.comm_semiring, one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast prod.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow prod.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, sup := idem_semiring.sup prod.idem_semiring, le := idem_semiring.le prod.idem_semiring, lt := idem_semiring.lt prod.idem_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot prod.idem_semiring, bot_le := _}

source

@[protected, instance]

def prod.kleene_algebra {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] :

kleene_algebra (α × β)

Equations

prod.kleene_algebra = {add := idem_semiring.add prod.idem_semiring, add_assoc := _, zero := idem_semiring.zero prod.idem_semiring, zero_add := _, add_zero := _, nsmul := idem_semiring.nsmul prod.idem_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := idem_semiring.mul prod.idem_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := idem_semiring.one prod.idem_semiring, one_mul := _, mul_one := _, nat_cast := idem_semiring.nat_cast prod.idem_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := idem_semiring.npow prod.idem_semiring, npow_zero' := _, npow_succ' := _, sup := idem_semiring.sup prod.idem_semiring, le := idem_semiring.le prod.idem_semiring, lt := idem_semiring.lt prod.idem_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot prod.idem_semiring, bot_le := _, kstar := λ (a : α × β), (has_kstar.kstar a.fst, has_kstar.kstar a.snd), one_le_kstar := _, mul_kstar_le_kstar := _, kstar_mul_le_kstar := _, mul_kstar_le_self := _, kstar_mul_le_self := _}

source

theorem prod.kstar_def {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :

has_kstar.kstar a = (has_kstar.kstar a.fst, has_kstar.kstar a.snd)

source

@[simp]

theorem prod.fst_kstar {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :

(has_kstar.kstar a).fst = has_kstar.kstar a.fst

source

@[simp]

theorem prod.snd_kstar {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :

(has_kstar.kstar a).snd = has_kstar.kstar a.snd

source

@[protected, instance]

def pi.idem_semiring {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), idem_semiring (π i)] :

idem_semiring (Π (i : ι), π i)

Equations

pi.idem_semiring = {add := semiring.add pi.semiring, add_assoc := _, zero := semiring.zero pi.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul pi.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul pi.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one pi.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast pi.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow pi.semiring, npow_zero' := _, npow_succ' := _, sup := semilattice_sup.sup pi.semilattice_sup, le := semilattice_sup.le pi.semilattice_sup, lt := semilattice_sup.lt pi.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := order_bot.bot pi.order_bot, bot_le := _}

source

@[protected, instance]

def pi.idem_comm_semiring {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), idem_comm_semiring (π i)] :

idem_comm_semiring (Π (i : ι), π i)

Equations

pi.idem_comm_semiring = {add := comm_semiring.add pi.comm_semiring, add_assoc := _, zero := comm_semiring.zero pi.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul pi.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul pi.comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one pi.comm_semiring, one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast pi.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow pi.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, sup := idem_semiring.sup pi.idem_semiring, le := idem_semiring.le pi.idem_semiring, lt := idem_semiring.lt pi.idem_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot pi.idem_semiring, bot_le := _}

source

@[protected, instance]

def pi.kleene_algebra {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] :

kleene_algebra (Π (i : ι), π i)

Equations

pi.kleene_algebra = {add := idem_semiring.add pi.idem_semiring, add_assoc := _, zero := idem_semiring.zero pi.idem_semiring, zero_add := _, add_zero := _, nsmul := idem_semiring.nsmul pi.idem_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := idem_semiring.mul pi.idem_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := idem_semiring.one pi.idem_semiring, one_mul := _, mul_one := _, nat_cast := idem_semiring.nat_cast pi.idem_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := idem_semiring.npow pi.idem_semiring, npow_zero' := _, npow_succ' := _, sup := idem_semiring.sup pi.idem_semiring, le := idem_semiring.le pi.idem_semiring, lt := idem_semiring.lt pi.idem_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot pi.idem_semiring, bot_le := _, kstar := λ (a : Π (i : ι), π i) (i : ι), has_kstar.kstar (a i), one_le_kstar := _, mul_kstar_le_kstar := _, kstar_mul_le_kstar := _, mul_kstar_le_self := _, kstar_mul_le_self := _}

source

theorem pi.kstar_def {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) :

has_kstar.kstar a = λ (i : ι), has_kstar.kstar (a i)

source

@[simp]

theorem pi.kstar_apply {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) (i : ι) :

has_kstar.kstar a i = has_kstar.kstar (a i)

source

@[protected, reducible]

def function.injective.idem_semiring {α : Type u_1} {β : Type u_2} [idem_semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :

idem_semiring β

Pullback an idem_semiring instance along an injective function.

Equations

function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot = {add := semiring.add (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := semiring.zero (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, sup := semilattice_sup.sup (function.injective.semilattice_sup f hf sup), le := semilattice_sup.le (function.injective.semilattice_sup f hf sup), lt := semilattice_sup.lt (function.injective.semilattice_sup f hf sup), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := ⊥, bot_le := _}

source

@[protected, reducible]

def function.injective.idem_comm_semiring {α : Type u_1} {β : Type u_2} [idem_comm_semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :

idem_comm_semiring β

Pullback an idem_comm_semiring instance along an injective function.

Equations

function.injective.idem_comm_semiring f hf zero one add mul nsmul npow nat_cast sup bot = {add := comm_semiring.add (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := comm_semiring.zero (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, mul_comm := _, sup := idem_semiring.sup (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), le := idem_semiring.le (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), lt := idem_semiring.lt (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), bot_le := _}

source

@[protected, reducible]

def function.injective.kleene_algebra {α : Type u_1} {β : Type u_2} [kleene_algebra α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] [has_kstar β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) (kstar : ∀ (a : β), f (has_kstar.kstar a) = has_kstar.kstar (f a)) :

kleene_algebra β

Pullback an idem_comm_semiring instance along an injective function.

Equations

function.injective.kleene_algebra f hf zero one add mul nsmul npow nat_cast sup bot kstar = {add := idem_semiring.add (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), add_assoc := _, zero := idem_semiring.zero (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), zero_add := _, add_zero := _, nsmul := idem_semiring.nsmul (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := idem_semiring.mul (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := idem_semiring.one (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), one_mul := _, mul_one := _, nat_cast := idem_semiring.nat_cast (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), nat_cast_zero := _, nat_cast_succ := _, npow := idem_semiring.npow (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), npow_zero' := _, npow_succ' := _, sup := idem_semiring.sup (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), le := idem_semiring.le (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), lt := idem_semiring.lt (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot (function.injective.idem_semiring f hf zero one add mul nsmul npow nat_cast sup bot), bot_le := _, kstar := has_kstar.kstar _inst_11, one_le_kstar := _, mul_kstar_le_kstar := _, kstar_mul_le_kstar := _, mul_kstar_le_self := _, kstar_mul_le_self := _}

mathlib3 documentation

Kleene Algebras #

Main declarations #

Notation #

References #

TODO #

Tags #