English
If α is a semiring with idempotent addition (a + a = a for all a), then α equipped with the same operations becomes an IdemSemiring.
Русский
Если α — полукольцо с идемпотентным сложением (для всех a выполняется a + a = a), то α с теми же операциями образует IdemSemiring.
LaTeX
$$$ (\forall a:\alpha,\ a + a = a) \implies \text{IdemSemiring } \alpha $$$
Lean4
/-- Construct an idempotent semiring from an idempotent addition. -/
abbrev ofSemiring [Semiring α] (h : ∀ a : α, a + a = a) : IdemSemiring α :=
{ ‹Semiring α› with
le := fun a b ↦ a + b = b
le_refl := h
le_trans := fun a b c hab hbc ↦ by rw [← hbc, ← add_assoc, hab]
le_antisymm := fun a b hab hba ↦ by rwa [← hba, add_comm]
sup := (· + ·)
le_sup_left := fun a b ↦ by rw [← add_assoc, h]
le_sup_right := fun a b ↦ by rw [add_comm, add_assoc, h]
sup_le := fun a b c hab hbc ↦ by rwa [add_assoc, hbc]
bot := 0
bot_le := zero_add }
