Custom operators

class Validate (α : Type u_1) : Type u_1

• validate : α → α

  Validate ▵

class Covalidate (α : Type u_1) : Type u_1

• covalidate : α → α

  Co-validate ▿

def «term_↜_» : Lean.TrailingParserDescr

Heyting co-implication ↜

Equations

• «term_↜_» = Lean.ParserDescr.trailingNode `«term_↜_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↜ ") (Lean.ParserDescr.cat `term 60))

def «term~_» : Lean.ParserDescr

Set / lattice complement

Equations

• «term~_» = Lean.ParserDescr.node `«term~_» 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~ ") (Lean.ParserDescr.cat `term 72))

def «term▵_» : Lean.ParserDescr

Validate ▵

Equations

• «term▵_» = Lean.ParserDescr.node `«term▵_» 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▵ ") (Lean.ParserDescr.cat `term 72))

def «term▿_» : Lean.ParserDescr

Co-validate ▿

Equations

• «term▿_» = Lean.ParserDescr.node `«term▿_» 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▿ ") (Lean.ParserDescr.cat `term 72))

@[implicit_reducible]

instance instValidateOfHNot {α : Type u_1} [HNot α] : Validate α

Equations

• instValidateOfHNot = { validate := fun (x : α) => ￢￢x }

@[implicit_reducible]

instance instCovalidateOfCompl {α : Type u_1} [Compl α] : Covalidate α

Equations

• instCovalidateOfCompl = { covalidate := fun (x : α) => ~ ~ x }

@[implicit_reducible]

noncomputable instance instSDiffForall_pGCL {α : Type u_1} {β : Type u_2} [SDiff β] : SDiff (α → β)

Equations

• instSDiffForall_pGCL = inferInstance

theorem ENNReal.hnot_def {a : ENNReal} : ￢a = if a = ⊤ then 0 else ⊤

theorem ENNReal.compl_def {a : ENNReal} : ~ a = if a = 0 then ⊤ else 0

theorem ENNReal.himp_def {a b : ENNReal} : a ⇨ b = if a ≤ b then ⊤ else b

theorem ENNReal.sdiff_def {a b : ENNReal} : a \ b = if a ≤ b then 0 else a

theorem ENNReal.covalidate_sdiff {a b : ENNReal} : ▿ (a \ b) = if a ≤ b then 0 else ⊤

theorem ENNReal.le_covalidate_sdiff {x a b : ENNReal} : x ≤ ▿ (a \ b) ↔ a ≤ b → x = 0

theorem ENNReal.le_covalidate_sdiff_of_lt {x a b : ENNReal} (h : b < a) : x ≤ ▿ (a \ b)

theorem ENNReal.validate_himp_le_of_lt {x a b : ENNReal} (h : b < a) : ▵ (a ⇨ b) ≤ x

@[simp]

theorem ENNReal.himp_zero_le (x y : ENNReal) : x ⇨ 0 ≤ y ↔ x = 0 → y = ⊤

@[simp]

theorem ENNReal.himp_zero_eq_zero (x : ENNReal) : x ⇨ 0 = 0 ↔ ¬x = 0

@[simp]

theorem ENNReal.sdiff_zero_eq_zero (x y : ENNReal) : x \ y = 0 ↔ x ≤ y

@[simp]

theorem ENNReal.max_sdiff (x y : ENNReal) : max x (y \ ⊤) = x

@[simp]

theorem ENNReal.lt_himp (x y z : ENNReal) (hx : x < ⊤) : x < y ⇨ z ↔ z < y → x < z

@[simp]

theorem ENNReal.zero_himp (x : ENNReal) : 0 ⇨ x = ⊤

@[implicit_reducible]

noncomputable instance instSDiffENNReal_pGCL : SDiff ENNReal

Equations

• instSDiffENNReal_pGCL = inferInstance

class Iverson (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

• iver : α → β

  Iverson brackets i[b]

def «termI[_]» : Lean.ParserDescr

Iverson brackets i[b]

Equations

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

class LawfulIverson (α : Type u_1) (β : outParam (Type u_2)) [Iverson α β] [LE β] [One β] : Prop

• iver_le_one (b : α) : i[b] ≤ 1

@[implicit_reducible]

instance Iverson.instBoolNat : Iverson Bool ℕ

Equations

• Iverson.instBoolNat = { iver := fun (b : Bool) => if b = true then 1 else 0 }

instance Iverson.instLawfulIversonBoolNat : LawfulIverson Bool ℕ

@[implicit_reducible]

noncomputable instance Iverson.instPropNat : Iverson Prop ℕ

Equations

• Iverson.instPropNat = { iver := fun (b : Prop) => have this := Classical.propDecidable b; if b then 1 else 0 }

instance Iverson.instLawfulIversonPropNat : LawfulIverson Prop ℕ

@[simp]

theorem Iverson.iver_true : i[true] = 1

@[simp]

theorem Iverson.iver_True : i[True] = 1

@[simp]

theorem Iverson.iver_false : i[false] = 0

@[simp]

theorem Iverson.iver_False : i[False] = 0

theorem Iverson.iver_neg {b : Prop} : i[¬b] = 1 - i[b]

theorem Iverson.iver_not {b : Bool} : i[!b] = 1 - i[b]

@[implicit_reducible]

instance Pi.instSubstitution {α : Type u_1} {β : Type u_2} {ι : Type u_3} {γ : ι → Type u_4} [Substitution α γ] : Substitution (α → β) fun (a : ι) => α → γ a

Equations

• Pi.instSubstitution = { subst := fun (f : α → β) (x : (a : ι) × (α → γ a)) (σ : α) => match x with | ⟨i, x⟩ => f (σ[i ↦ x σ]) }

@[simp]

theorem Pi.substs_cons {α : Type u_1} {β : Type u_2} {ι : Type u_3} {γ : ι → Type u_4} [Substitution α γ] {σ : α} (f : α → β) (x₀ : (a : ι) × (α → γ a)) (xs : List ((a : ι) × (α → γ a))) : (f[..x₀ :: xs]) σ = (f[..xs]) (σ[x₀.fst ↦ x₀.snd σ])

@[implicit_reducible]

noncomputable instance Pi.instIverson {α : Type u_1} : Iverson (α → Prop) (α → ENNReal)

Equations

• Pi.instIverson = { iver := fun (v : α → Prop) (σ : α) => ↑i[v σ] }

@[implicit_reducible]

noncomputable instance Pi.instIversonBool {α : Type u_1} : Iverson (α → Bool) (α → ENNReal)

Equations

• Pi.instIversonBool = { iver := fun (v : α → Bool) (σ : α) => ↑i[v σ] }

@[simp]

theorem Pi.iver_prop_apply {α : Type u_1} {f : α → Prop} {σ : α} : i[f] σ = ↑i[f σ]

@[simp]

theorem Pi.iver_bool_apply {α : Type u_1} {f : α → Bool} {σ : α} : i[f] σ = ↑i[f σ]

instance Pi.instLawfulIverson {α : Type u_1} : LawfulIverson (α → Prop) (α → ENNReal)

instance Pi.instLawfulIversonBool {α : Type u_1} : LawfulIverson (α → Bool) (α → ENNReal)

@[simp]

theorem Pi.iver_subst {α : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Substitution α γ] (f : α → Prop) (x : ι) (y : α → γ x) : i[f][x ↦ y] = i[f[x ↦ y]]

@[simp]

theorem Pi.iver_bool_subst {α : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Substitution α γ] (f : α → Bool) (x : ι) (y : α → γ x) : i[f][x ↦ y] = i[f[x ↦ y]]

@[simp]

theorem Pi.iver_True {α : Type u_1} : i[fun (x : α) => True] = 1

@[simp]

theorem Pi.iver_True_compl {α : Type u_1} : i[~ fun (x : α) => True] = 0

@[simp]

theorem Pi.iver_False {α : Type u_1} : i[fun (x : α) => False] = 0

@[simp]

theorem Pi.iver_False_compl {α : Type u_1} : i[~ fun (x : α) => False] = 1

@[simp]

theorem Pi.iver_bool_eq_true {b : Bool} : i[b = true] = i[b]

@[simp]

theorem Pi.iver_bool_eq_false {b : Bool} : i[b = false] = i[¬b = true]

@[simp]

theorem ENNReal.iver_eq_zero_himp_le (x y z : ENNReal) (hz : z ≠ ⊤) : ↑i[x = 0] * ⊤ ⇨ y ≤ z ↔ x = 0 ∧ y ≤ z

Expressions & State

def pGCL.«termΓ[_]» : Lean.ParserDescr

Equations

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

def pGCL.State {𝒱 : Type u_1} (Γ : 𝒱 → Type u_2) : Type (max u_1 u_2)

Equations

• pGCL.State Γ = ((s : 𝒱) → Γ s)

def pGCL.«term𝔼[_,_]» : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance pGCL.State.instSubstitution {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] : Substitution (State Γ) Γ

Equations

• pGCL.State.instSubstitution = { subst := fun (σ : pGCL.State Γ) (x : Sigma Γ) (α : 𝒱) => match x with | ⟨v, t⟩ => if h : v = α then cast ⋯ t else σ α }

theorem pGCL.State.ext {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ₁ σ₂ : State Γ} (h : ∀ (v : 𝒱), σ₁ v = σ₂ v) : σ₁ = σ₂

theorem pGCL.State.ext_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ₁ σ₂ : State Γ} : σ₁ = σ₂ ↔ ∀ (v : 𝒱), σ₁ v = σ₂ v

@[simp]

theorem pGCL.State.subst_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {x : 𝒱} {v : Γ x} {y : 𝒱} [DecidableEq 𝒱] {σ : State Γ} : (σ[x ↦ v]) y = if h : x = y then cast ⋯ v else σ y

instance pGCL.Exp.instAddLeftMonoForall_pGCL {α : Type u_4} {ι : Type u_3} [Add α] [LE α] [AddLeftMono α] : AddLeftMono (ι → α)

instance pGCL.Exp.instAddRightMonoForall_pGCL {α : Type u_4} {ι : Type u_3} [Add α] [LE α] [AddRightMono α] : AddRightMono (ι → α)

@[simp]

theorem pGCL.Exp.add_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Add α] : (a + b)[..xs] = a[..xs] + b[..xs]

@[simp]

theorem pGCL.Exp.sub_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Sub α] : (a - b)[..xs] = a[..xs] - b[..xs]

@[simp]

theorem pGCL.Exp.mul_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Mul α] : (a * b)[..xs] = a[..xs] * b[..xs]

@[simp]

theorem pGCL.Exp.div_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Div α] : (a / b)[..xs] = a[..xs] / b[..xs]

@[simp]

theorem pGCL.Exp.max_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Max α] : (a ⊔ b)[..xs] = a[..xs] ⊔ b[..xs]

@[simp]

theorem pGCL.Exp.min_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [Min α] : (a ⊓ b)[..xs] = a[..xs] ⊓ b[..xs]

@[simp]

theorem pGCL.Exp.himp_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [HImp α] : (a ⇨ b)[..xs] = a[..xs] ⇨ b[..xs]

@[simp]

theorem pGCL.Exp.sdiff_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → α} [DecidableEq 𝒱] {xs : List ((a : 𝒱) × (State Γ → Γ a))} [SDiff α] : (b \ a)[..xs] = b[..xs] \ a[..xs]

@[simp]

theorem pGCL.Exp.validate_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} [HNot α] {φ : State Γ → α} : (▵ φ) σ = ▵ φ σ

@[simp]

theorem pGCL.Exp.covalidate_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} [Compl α] {φ : State Γ → α} : (▿ φ) σ = ▿ φ σ

@[simp]

theorem pGCL.Exp.subst_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} [DecidableEq 𝒱] (e : State Γ → α) (x : 𝒱) (A : State Γ → Γ x) : (e[x ↦ A]) σ = e (σ[x ↦ A σ])

@[simp]

theorem pGCL.Exp.subst₂_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {y : 𝒱} {B : State Γ → Γ y} {σ : State Γ} [DecidableEq 𝒱] (e : State Γ → α) (x : 𝒱) (A : State Γ → Γ x) : (e[x ↦ A, y ↦ B]) σ = e (σ[y ↦ B (σ[x ↦ A σ]), x ↦ A σ])

theorem pGCL.Exp.add_le_add {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] (a b c d : State Γ → α) (hac : a ≤ c) (hbd : b ≤ d) : a + b ≤ c + d

theorem pGCL.Exp.mul_le_mul {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a b c d : State Γ → α) (hac : a ≤ c) (hbd : b ≤ d) : a * b ≤ c * d

@[reducible, inline]

abbrev pGCL.BExpr {𝒱 : Type u_1} (Γ : 𝒱 → Type u_3) : Type (max u_3 u_1)

Equations

• pGCL.BExpr Γ = (pGCL.State Γ → Prop)

noncomputable def pGCL.BExpr.forall_ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (x : 𝒱) (b : BExpr Γ) : BExpr Γ

Equations

• pGCL.BExpr.forall_ x b σ = ∀ (v : Γ x), b (σ[x ↦ v])

noncomputable def pGCL.BExpr.exists_ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (x : 𝒱) (b : BExpr Γ) : BExpr Γ

Equations

• pGCL.BExpr.exists_ x b σ = ∃ (v : Γ x), b (σ[x ↦ v])

@[implicit_reducible]

instance pGCL.BExpr.instHNot {𝒱✝ : Type u_3} {α : 𝒱✝ → Type u_4} : HNot (BExpr α)

Equations

• pGCL.BExpr.instHNot = { hnot := compl }

def pGCL.BExpr.coe_prop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Prop → BExpr Γ

Equations

• ↑b x✝ = b

@[implicit_reducible]

instance pGCL.BExpr.instCoePropForallState {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Coe Prop (State Γ → Prop)

Equations

• pGCL.BExpr.instCoePropForallState = { coe := pGCL.BExpr.coe_prop }

@[simp]

theorem pGCL.BExpr.coe_prop_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} {b : Prop} : ↑b σ = b

@[simp]

theorem pGCL.BExpr.iver_mul_le_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {σ : State Γ} {X : State Γ → ENNReal} : ↑i[b σ] * X σ ≤ X σ

@[simp]

theorem pGCL.BExpr.iver_mul_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {X : State Γ → ENNReal} : i[b] * X ≤ X

@[simp]

theorem pGCL.BExpr.mul_iver_le_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {σ : State Γ} {X : State Γ → ENNReal} : X σ * ↑i[b σ] ≤ X σ

@[simp]

theorem pGCL.BExpr.mul_iver_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {X : State Γ → ENNReal} : X * i[b] ≤ X

noncomputable def pGCL.BExpr.lt {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [PartialOrder α] (l r : State Γ → α) : BExpr Γ

Equations

• pGCL.BExpr.lt l r σ = (l σ < r σ)

noncomputable def pGCL.BExpr.le {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [PartialOrder α] (l r : State Γ → α) : BExpr Γ

Equations

• pGCL.BExpr.le l r σ = (l σ ≤ r σ)

noncomputable def pGCL.BExpr.eq {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (l r : State Γ → α) : BExpr Γ

Equations

• pGCL.BExpr.eq l r σ = (l σ = r σ)

def pGCL.BExpr.and {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (l r : BExpr Γ) : BExpr Γ

Equations

• l.and r σ = (l σ ∧ r σ)

def pGCL.BExpr.or {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (l r : BExpr Γ) : BExpr Γ

Equations

• l.or r σ = (l σ ∨ r σ)

noncomputable def pGCL.BExpr.ite {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (b l r : BExpr Γ) : BExpr Γ

Equations

• b.ite l r σ = if b σ then l σ else r σ

@[simp]

theorem pGCL.BExpr.lt_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [PartialOrder α] {σ : State Γ} {l r : State Γ → α} : lt l r σ ↔ l σ < r σ

@[simp]

theorem pGCL.BExpr.le_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [PartialOrder α] {σ : State Γ} {l r : State Γ → α} : le l r σ ↔ l σ ≤ r σ

@[simp]

theorem pGCL.BExpr.eq_apply {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} {l r : State Γ → α} : eq l r σ ↔ l σ = r σ

@[simp]

theorem pGCL.BExpr.and_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} {l r : BExpr Γ} : l.and r σ ↔ l σ ∧ r σ

@[simp]

theorem pGCL.BExpr.or_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} {l r : BExpr Γ} : l.or r σ ↔ l σ ∨ r σ

@[simp]

theorem pGCL.BExpr.ite_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {σ : State Γ} (b l r : BExpr Γ) : b.ite l r σ = if b σ then l σ else r σ

@[simp]

theorem pGCL.BExpr.eq_subst {α : Type u_3} {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {xs : List ((a : 𝒱) × (State Γ → Γ a))} [DecidableEq 𝒱] {a b : State Γ → α} : (eq a b)[..xs] = eq (a[..xs]) (b[..xs])

instance OrderHom.instAddLeftMonoForallStateENNReal {𝒱✝ : Type u_3} {Γ : 𝒱✝ → Type u_4} : AddLeftMono (pGCL.State Γ → ENNReal)

instance OrderHom.instAddRightMonoForallStateENNReal {𝒱✝ : Type u_3} {Γ : 𝒱✝ → Type u_4} : AddRightMono (pGCL.State Γ → ENNReal)

@[implicit_reducible]

instance OrderHom.instAdd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [Add β] [AddLeftMono β] [AddRightMono β] : Add (α →o β)

Equations

• OrderHom.instAdd = { add := fun (a b : α →o β) => { toFun := fun (x : α) => a x + b x, monotone' := ⋯ } }

@[simp]

theorem OrderHom.add_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [Add β] [AddLeftMono β] [AddRightMono β] {x : α} (f g : α →o β) : (f + g) x = f x + g x

@[simp]

theorem OrderHom.add_apply2' {α : Type u_1} [Preorder α] {𝒱✝ : Type u_3} {Γ : 𝒱✝ → Type u_4} {x : α} {y : pGCL.State Γ} (f g : α →o pGCL.State Γ → ENNReal) : (f + g) x y = f x y + g x y

@[implicit_reducible]

instance OrderHom.instOfNat_pGCL {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {n : ℕ} [OfNat β n] : OfNat (α →o β) n

Equations

• OrderHom.instOfNat_pGCL = { ofNat := { toFun := fun (x : α) => OfNat.ofNat n, monotone' := ⋯ } }

@[simp]

theorem OrderHom.ofNat_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {n : ℕ} {a : α} [OfNat β n] : (OfNat.ofNat n) a = OfNat.ofNat n

@[implicit_reducible]

instance OrderHom.instAddZeroClassOfAddLeftMonoOfAddRightMono_pGCL {α : Type u_1} [Preorder α] {β : Type u_3} [Preorder β] [AddZeroClass β] [AddLeftMono β] [AddRightMono β] : AddZeroClass (α →o β)

Equations

• OrderHom.instAddZeroClassOfAddLeftMonoOfAddRightMono_pGCL = { toZero := Zero.ofOfNat0, toAdd := OrderHom.instAdd, zero_add := ⋯, add_zero := ⋯ }

instance OrderHom.instAddRightMonoForall_pGCL {α : Type u_3} {β : Type u_4} [Preorder β] [Add β] [i : AddRightMono β] : AddRightMono (α → β)

instance OrderHom.instAddLeftMonoForall_pGCL {α : Type u_3} {β : Type u_4} [Preorder β] [Add β] [i : AddLeftMono β] : AddLeftMono (α → β)

@[simp]

theorem OrderHom.mk_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {ι : Type u_3} {a : α} {f : α → ι → β} {h : Monotone f} {b : ι} : { toFun := f, monotone' := h } a b = f a b

@[simp]

theorem OrderHom.mk_apply' {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {ι : Type u_3} {a : α} {f : α → ι → β} {h : Monotone f} {b : ι} : { toFun := f, monotone' := h } a b = f a b

@[simp]

theorem OrderHom.comp_apply' {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {ι : Type u_4} {γ : Type u_5} [Preorder γ] {f : β →o ι → γ} {g : α →o β} {b : ι} : (f.comp g) a b = f (g a) b