structure MinMax (α : Type) : Type

• val : α

theorem MinMax.ext {α : Type} {x y : MinMax α} (val : x.val = y.val) : x = y

theorem MinMax.ext_iff {α : Type} {x y : MinMax α} : x = y ↔ x.val = y.val

instance instCoeMinMax {α : Type} : Coe (MinMax α) α

Equations

• instCoeMinMax = { coe := MinMax.val }

instance instTopMinMax {α : Type} [LinearOrder α] [OrderTop α] : Top (MinMax α)

Equations

• instTopMinMax = { top := { val := ⊤ } }

instance instBotMinMax {α : Type} [LinearOrder α] [OrderBot α] : Bot (MinMax α)

Equations

• instBotMinMax = { bot := { val := ⊥ } }

instance instLEMinMax {α : Type} [LinearOrder α] : LE (MinMax α)

Equations

• instLEMinMax = { le := fun (a b : MinMax α) => b.val ≤ a.val }

instance instLinearOrderMinMax {α : Type} [LinearOrder α] : LinearOrder (MinMax α)

Equations

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

instance instZeroMinMax {α : Type} [LinearOrder α] [OrderTop α] : Zero (MinMax α)

Equations

• instZeroMinMax = { zero := ⊤ }

instance instAddMinMax {α : Type} [LinearOrder α] : Add (MinMax α)

Equations

• instAddMinMax = { add := fun (a b : MinMax α) => { val := min a.val b.val } }

instance instOneMinMax {α : Type} [LinearOrder α] [OrderBot α] : One (MinMax α)

Equations

• instOneMinMax = { one := ⊥ }

instance instMulMinMax {α : Type} [LinearOrder α] : Mul (MinMax α)

Equations

• instMulMinMax = { mul := fun (a b : MinMax α) => { val := max a.val b.val } }

instance instSubMinMax {α : Type} [LinearOrder α] [OrderTop α] : Sub (MinMax α)

Equations

• instSubMinMax = { sub := fun (a b : MinMax α) => if a.val ≥ b.val then { val := ⊤ } else { val := a.val } }

instance instCommSemiringMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiring (MinMax α)

Equations

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

instance instSemiringWithMonusMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : SemiringWithMonus (MinMax α)

Equations

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

theorem MinMax.absorptive {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : _root_.absorptive (MinMax α)

theorem MinMax.idempotent {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : _root_.idempotent (MinMax α)

@[reducible, inline]

abbrev MaxMin (α : Type) : Type

Equations

• MaxMin α = MinMax αᵒᵈ

instance instCommSemiringMaxMin {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiring (MaxMin α)

Equations

• instCommSemiringMaxMin = inferInstanceAs (CommSemiring (MinMax αᵒᵈ))

instance instSemiringWithMonusMaxMin {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : SemiringWithMonus (MaxMin α)

Equations

• instSemiringWithMonusMaxMin = inferInstanceAs (SemiringWithMonus (MinMax αᵒᵈ))

inductive TVL : Type

• bot : TVL
• unknown : TVL
• top : TVL

instance instDecidableEqTVL : DecidableEq TVL

Equations

• instDecidableEqTVL x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instReprTVL : Repr TVL

Equations

• instReprTVL = { reprPrec := instReprTVL.repr }

def instReprTVL.repr : TVL → ℕ → Std.Format

Equations

• instReprTVL.repr TVL.bot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.bot")).group prec✝
• instReprTVL.repr TVL.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.unknown")).group prec✝
• instReprTVL.repr TVL.top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.top")).group prec✝

def instOrdTVL.ord : TVL → TVL → Ordering

Equations

• instOrdTVL.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

instance instOrdTVL : Ord TVL

Equations

• instOrdTVL = { compare := instOrdTVL.ord }

instance instLETVL : LE TVL

Equations

• instLETVL = { le := fun (a b : TVL) => (compare a b).isLE = true }

instance instLinearOrderTVL : LinearOrder TVL

Equations

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

instance instOrderBotTVL : OrderBot TVL

Equations

• instOrderBotTVL = { bot := TVL.bot, bot_le := instOrderBotTVL._proof_1 }

instance instOrderTopTVL : OrderTop TVL

Equations

• instOrderTopTVL = { top := TVL.top, le_top := instOrderTopTVL._proof_1 }

instance instCommSemiringMaxMinTVL : CommSemiring (MaxMin TVL)

Equations

• instCommSemiringMaxMinTVL = inferInstance

instance instSemiringWithMonusMaxMinTVL : SemiringWithMonus (MaxMin TVL)

Equations

• instSemiringWithMonusMaxMinTVL = inferInstance

theorem TVL.not_mul_sub_left_distributive : ¬mul_sub_left_distributive (MaxMin TVL)