@[reducible, inline]

abbrev Lukasiewicz : Type

Equations

• Lukasiewicz = { q : ℚ // 0 ≤ q ∧ q ≤ 1 }

instance instZeroLukasiewicz : Zero Lukasiewicz

Equations

• instZeroLukasiewicz = { zero := ⟨0, instZeroLukasiewicz._proof_1⟩ }

instance instOneLukasiewicz : One Lukasiewicz

Equations

• instOneLukasiewicz = { one := ⟨1, instOneLukasiewicz._proof_1⟩ }

instance instAddLukasiewicz : Add Lukasiewicz

Equations

• instAddLukasiewicz = { add := fun (a b : Lukasiewicz) => max a b }

instance instMulLukasiewicz : Mul Lukasiewicz

Equations

• instMulLukasiewicz = { mul := fun (a b : Lukasiewicz) => let raw := max (↑a + ↑b - 1) 0; have h := ⋯; ⟨raw, h⟩ }

instance instSubLukasiewicz : Sub Lukasiewicz

Equations

• instSubLukasiewicz = { sub := fun (a b : Lukasiewicz) => if a ≤ b then ⟨0, instZeroLukasiewicz._proof_1⟩ else a }

theorem Lukasiewicz.sub_def (a b : Lukasiewicz) : a - b = if a ≤ b then ⟨0, ⋯⟩ else a

instance instCommMagmaLukasiewicz : CommMagma Lukasiewicz

Equations

• instCommMagmaLukasiewicz = { toMul := instMulLukasiewicz, mul_comm := instCommMagmaLukasiewicz._proof_1 }

instance instLeftDistribClassLukasiweicz : LeftDistribClass Lukasiewicz

instance instCommSemiringLukasiewicz : CommSemiring Lukasiewicz

Equations

• One or more equations did not get rendered due to their size.

instance instLinearOrderLukasiewicz : LinearOrder Lukasiewicz

Equations

• One or more equations did not get rendered due to their size.

instance instIsOrderedAddMonoidLukasiewicz : IsOrderedAddMonoid Lukasiewicz

instance instCanonicallyOrderedAddLukasiewicz : CanonicallyOrderedAdd Lukasiewicz

instance instSemiringWithMonusLukasiewicz : SemiringWithMonus Lukasiewicz

Equations

• One or more equations did not get rendered due to their size.

theorem Lukasiewicz.absorptive : _root_.absorptive Lukasiewicz

theorem Lukasiewicz.idempotent : _root_.idempotent Lukasiewicz

theorem Lukasiewicz.mul_sub_left_distributive : _root_.mul_sub_left_distributive Lukasiewicz