Pi instances for ordered groups and monoids

This file defines instances for ordered group, monoid, and related structures on Pi types.

ink

def Pi.orderedAddCommMonoid.proof_2 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : (i : ι) → Z i), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : (i : ι) → Z i), a ≤ b → b ≤ a → a = b)

ink

def Pi.orderedAddCommMonoid.proof_3 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] : ∀ (x x_1 : (i : ι) → Z i), x ≤ x_1 → ∀ (x_2 : (i : ι) → Z i) (i : ι), x_2 i + x i ≤ x_2 i + x_1 i

Equations

• (_ : x i + x i ≤ x i + x i) = (_ : x i + x i ≤ x i + x i)

ink

instance Pi.orderedAddCommMonoid {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] : OrderedAddCommMonoid ((i : ι) → Z i)

The product of a family of ordered additive commutative monoids is an ordered additive commutative monoid.

Equations

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

ink

def Pi.orderedAddCommMonoid.proof_1 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : ι) → Z i), a + b = b + a) = (_ : ∀ (a b : (i : ι) → Z i), a + b = b + a)

ink

instance Pi.orderedCommMonoid {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → OrderedCommMonoid (Z i)] : OrderedCommMonoid ((i : ι) → Z i)

The product of a family of ordered commutative monoids is an ordered commutative monoid.

Equations

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

ink

instance Pi.existsAddOfLe {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Add (α i)] [inst : ∀ (i : ι), ExistsAddOfLE (α i)] : ExistsAddOfLE ((i : ι) → α i)

Equations

• @Pi.existsAddOfLe = @Pi.existsAddOfLe.proof_1

ink

def Pi.existsAddOfLe.proof_1 {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Add (α i)] [inst : ∀ (i : ι), ExistsAddOfLE (α i)] : ExistsAddOfLE ((i : ι) → α i)

Equations

• (_ : ExistsAddOfLE ((i : ι) → α i)) = (_ : ExistsAddOfLE ((i : ι) → α i))

ink

instance Pi.existsMulOfLe {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Mul (α i)] [inst : ∀ (i : ι), ExistsMulOfLE (α i)] : ExistsMulOfLE ((i : ι) → α i)

Equations

• @Pi.existsMulOfLe = @Pi.existsMulOfLe.proof_1

ink

def Pi.instCanonicallyOrderedAddMonoidForAll.proof_5 {ι : Type u_2} {Z : ι → Type u_1} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] : ∀ (x x_1 : (i : ι) → Z i) (x_2 : ι), x x_2 ≤ x x_2 + x_1 x_2

Equations

• (_ : x x ≤ x x + x x) = (_ : x x ≤ x x + x x)

ink

def Pi.instCanonicallyOrderedAddMonoidForAll.proof_4 {ι : Type u_2} {Z : ι → Type u_1} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] : ∀ {a b : (i : ι) → Z i}, a ≤ b → ∃ c, b = a + c

Equations

• (_ : a ≤ b → ∃ c, b = a + c) = (_ : a ≤ b → ∃ c, b = a + c)

ink

def Pi.instCanonicallyOrderedAddMonoidForAll.proof_3 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] (a : (i : ι) → Z i) : ⊥ ≤ a

Equations

• (_ : ∀ (a : (i : ι) → Z i), ⊥ ≤ a) = (_ : ∀ (a : (i : ι) → Z i), ⊥ ≤ a)

ink

def Pi.instCanonicallyOrderedAddMonoidForAll.proof_2 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) : a ≤ b → ∀ (c : (i : ι) → Z i), c + a ≤ c + b

Equations

• (_ : ∀ (a b : (i : ι) → Z i), a ≤ b → ∀ (c : (i : ι) → Z i), c + a ≤ c + b) = (_ : ∀ (a b : (i : ι) → Z i), a ≤ b → ∀ (c : (i : ι) → Z i), c + a ≤ c + b)

ink

instance Pi.instCanonicallyOrderedAddMonoidForAll {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] : CanonicallyOrderedAddMonoid ((i : ι) → Z i)

The product of a family of canonically ordered additive monoids is a canonically ordered additive monoid.

Equations

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

ink

def Pi.instCanonicallyOrderedAddMonoidForAll.proof_1 {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] : ExistsAddOfLE ((i : ι) → Z i)

Equations

• (_ : ExistsAddOfLE ((i : ι) → Z i)) = (_ : ExistsAddOfLE ((i : ι) → Z i))

ink

instance Pi.instCanonicallyOrderedMonoidForAll {ι : Type u_1} {Z : ι → Type u_2} [inst : (i : ι) → CanonicallyOrderedMonoid (Z i)] : CanonicallyOrderedMonoid ((i : ι) → Z i)

The product of a family of canonically ordered monoids is a canonically ordered monoid.

Equations

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

ink

def Pi.orderedAddCancelCommMonoid.proof_1 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

def Pi.orderedAddCancelCommMonoid.proof_10 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : (i : I) → f i), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : (i : I) → f i), a ≤ b → b ≤ a → a = b)

ink

def Pi.orderedAddCancelCommMonoid.proof_11 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] : ∀ (x x_1 : (i : I) → f i), x ≤ x_1 → ∀ (h : (i : I) → f i) (i : I), h i + x i ≤ h i + x_1 i

Equations

• (_ : h i + x i ≤ h i + x i) = (_ : h i + x i ≤ h i + x i)

ink

def Pi.orderedAddCancelCommMonoid.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def Pi.orderedAddCancelCommMonoid.proof_8 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a ≤ b → b ≤ c → a ≤ c

Equations

• (_ : ∀ (a b c : (i : I) → f i), a ≤ b → b ≤ c → a ≤ c) = (_ : ∀ (a b c : (i : I) → f i), a ≤ b → b ≤ c → a ≤ c)

ink

def Pi.orderedAddCancelCommMonoid.proof_9 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a < b ↔ a ≤ b ∧ ¬b ≤ a

Equations

• (_ : ∀ (a b : (i : I) → f i), a < b ↔ a ≤ b ∧ ¬b ≤ a) = (_ : ∀ (a b : (i : I) → f i), a < b ↔ a ≤ b ∧ ¬b ≤ a)

ink

def Pi.orderedAddCancelCommMonoid.proof_7 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) : a ≤ a

Equations

• (_ : ∀ (a : (i : I) → f i), a ≤ a) = (_ : ∀ (a : (i : I) → f i), a ≤ a)

ink

def Pi.orderedAddCancelCommMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

instance Pi.orderedAddCancelCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] : OrderedCancelAddCommMonoid ((i : I) → f i)

Equations

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

ink

def Pi.orderedAddCancelCommMonoid.proof_6 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.orderedAddCancelCommMonoid.proof_12 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] : ∀ (x x_1 x_2 : (i : I) → f i), x + x_1 ≤ x + x_2 → ∀ (i : I), x_1 i ≤ x_2 i

Equations

• (_ : x i ≤ x i) = (_ : x i ≤ x i)

ink

def Pi.orderedAddCancelCommMonoid.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

def Pi.orderedAddCancelCommMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

instance Pi.orderedCancelCommMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedCancelCommMonoid (f i)] : OrderedCancelCommMonoid ((i : I) → f i)

Equations

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

ink

def Pi.orderedAddCommGroup.proof_9 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

Equations

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

ink

def Pi.orderedAddCommGroup.proof_6 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a - b = a + -b

Equations

• (_ : ∀ (a b : (i : I) → f i), a - b = a + -b) = (_ : ∀ (a b : (i : I) → f i), a - b = a + -b)

ink

def Pi.orderedAddCommGroup.proof_14 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a < b ↔ a ≤ b ∧ ¬b ≤ a

Equations

• (_ : ∀ (a b : (i : I) → f i), a < b ↔ a ≤ b ∧ ¬b ≤ a) = (_ : ∀ (a b : (i : I) → f i), a < b ↔ a ≤ b ∧ ¬b ≤ a)

ink

def Pi.orderedAddCommGroup.proof_12 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) : a ≤ a

Equations

• (_ : ∀ (a : (i : I) → f i), a ≤ a) = (_ : ∀ (a : (i : I) → f i), a ≤ a)

ink

def Pi.orderedAddCommGroup.proof_3 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) : a + 0 = a

Equations

• (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)

ink

def Pi.orderedAddCommGroup.proof_2 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) : 0 + a = a

Equations

• (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)

ink

instance Pi.orderedAddCommGroup {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedAddCommGroup (f i)] : OrderedAddCommGroup ((i : I) → f i)

Equations

• Pi.orderedAddCommGroup = let src := Pi.addCommGroup; let src_1 := Pi.orderedAddCommMonoid; OrderedAddCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a ≤ b → ∀ (c : (i : I) → f i), c + a ≤ c + b)

ink

def Pi.orderedAddCommGroup.proof_5 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (x : (i : I) → f i) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def Pi.orderedAddCommGroup.proof_15 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : (i : I) → f i), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : (i : I) → f i), a ≤ b → b ≤ a → a = b)

ink

def Pi.orderedAddCommGroup.proof_13 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a ≤ b → b ≤ c → a ≤ c

Equations

• (_ : ∀ (a b c : (i : I) → f i), a ≤ b → b ≤ c → a ≤ c) = (_ : ∀ (a b c : (i : I) → f i), a ≤ b → b ≤ c → a ≤ c)

ink

def Pi.orderedAddCommGroup.proof_11 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a + b = b + a

Equations

• (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)

ink

def Pi.orderedAddCommGroup.proof_16 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) : a ≤ b → ∀ (c : (i : I) → f i), c + a ≤ c + b

Equations

• (_ : ∀ (a b : (i : I) → f i), a ≤ b → ∀ (c : (i : I) → f i), c + a ≤ c + b) = (_ : ∀ (a b : (i : I) → f i), a ≤ b → ∀ (c : (i : I) → f i), c + a ≤ c + b)

ink

def Pi.orderedAddCommGroup.proof_10 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) : -a + a = 0

Equations

• (_ : ∀ (a : (i : I) → f i), -a + a = 0) = (_ : ∀ (a : (i : I) → f i), -a + a = 0)

ink

def Pi.orderedAddCommGroup.proof_8 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (a : (i : I) → f i) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

Equations

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

ink

def Pi.orderedAddCommGroup.proof_7 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) : SubNegMonoid.zsmul 0 a = 0

Equations

• (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0)

ink

def Pi.orderedAddCommGroup.proof_4 {I : Type u_1} {f : I → Type u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (x : (i : I) → f i) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)

ink

def Pi.orderedAddCommGroup.proof_1 {I : Type u_2} {f : I → Type u_1} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) : a + b + c = a + (b + c)

Equations

• (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))

ink

instance Pi.orderedCommGroup {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedCommGroup (f i)] : OrderedCommGroup ((i : I) → f i)

Equations

• Pi.orderedCommGroup = let src := Pi.commGroup; let src_1 := Pi.orderedCommMonoid; OrderedCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a ≤ b → ∀ (c : (i : I) → f i), c * a ≤ c * b)

ink

instance Pi.orderedSemiring {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedSemiring (f i)] : OrderedSemiring ((i : I) → f i)

Equations

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

ink

instance Pi.orderedCommSemiring {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedCommSemiring (f i)] : OrderedCommSemiring ((i : I) → f i)

Equations

• Pi.orderedCommSemiring = let src := Pi.commSemiring; let src_1 := Pi.orderedSemiring; OrderedCommSemiring.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

instance Pi.orderedRing {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedRing (f i)] : OrderedRing ((i : I) → f i)

Equations

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

ink

instance Pi.orderedCommRing {I : Type u} {f : I → Type v} [inst : (i : I) → OrderedCommRing (f i)] : OrderedCommRing ((i : I) → f i)

Equations

• Pi.orderedCommRing = let src := Pi.commRing; let src_1 := Pi.orderedRing; OrderedCommRing.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

ink

theorem Function.const_nonneg_of_nonneg {α : Type u_1} (β : Type u_2) [inst : Zero α] [inst : Preorder α] {a : α} (ha : 0 ≤ a) : 0 ≤ Function.const β a

ink

theorem Function.one_le_const_of_one_le {α : Type u_1} (β : Type u_2) [inst : One α] [inst : Preorder α] {a : α} (ha : 1 ≤ a) : 1 ≤ Function.const β a

ink

theorem Function.const_nonpos_of_nonpos {α : Type u_1} (β : Type u_2) [inst : Zero α] [inst : Preorder α] {a : α} (ha : a ≤ 0) : Function.const β a ≤ 0

ink

theorem Function.const_le_one_of_le_one {α : Type u_1} (β : Type u_2) [inst : One α] [inst : Preorder α] {a : α} (ha : a ≤ 1) : Function.const β a ≤ 1

ink

@[simp]

theorem Function.const_nonneg {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] : 0 ≤ Function.const β a ↔ 0 ≤ a

ink

@[simp]

theorem Function.one_le_const {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] : 1 ≤ Function.const β a ↔ 1 ≤ a

ink

@[simp]

theorem Function.const_pos {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] : 0 < Function.const β a ↔ 0 < a

ink

@[simp]

theorem Function.one_lt_const {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] : 1 < Function.const β a ↔ 1 < a

ink

@[simp]

theorem Function.const_nonpos {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] : Function.const β a ≤ 0 ↔ a ≤ 0

ink

@[simp]

theorem Function.const_le_one {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] : Function.const β a ≤ 1 ↔ a ≤ 1

ink

@[simp]

theorem Function.const_neg {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] : Function.const β a < 0 ↔ a < 0

ink

@[simp]

theorem Function.const_lt_one {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] : Function.const β a < 1 ↔ a < 1