Ordered instances on submonoids

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_1 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

@[instance 75]

instance AddSubmonoidClass.toOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedAddCommMonoid ↥s

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedAddCommMonoid s = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : ↥s) => ↑a

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : ↥s), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : ↥s) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

@[instance 75]

instance SubmonoidClass.toOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCommMonoid ↥s

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• SubmonoidClass.toOrderedCommMonoid s = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) : ∀ (x x_1 : ↥s), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) : ∀ (x x_1 : ↥s), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : ↥s) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : ↥s), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : ↥s) => ↑a

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedAddCommMonoid ↥s

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedAddCommMonoid s = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

@[instance 75]

instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCommMonoid ↥s

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCommMonoid s = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

@[instance 75]

instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedCancelAddCommMonoid ↥s

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedCancelAddCommMonoid s = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : ↥s) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : ↥s), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : ↥s) => ↑a

@[instance 75]

instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCancelCommMonoid ↥s

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• SubmonoidClass.toOrderedCancelCommMonoid s = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : ↥s), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : ↥s) => ↑a

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : ↥s) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedCancelAddCommMonoid ↥s

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid s = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) : ∀ (x x_1 : ↥s), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) : ∀ (x x_1 : ↥s), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

@[instance 75]

instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCancelCommMonoid ↥s

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCancelCommMonoid s = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_2 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_1 {M : Type u_1} [OrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_3 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoid.toOrderedAddCommMonoid {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : OrderedAddCommMonoid ↥S

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• S.toOrderedAddCommMonoid = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance Submonoid.toOrderedCommMonoid {M : Type u_1} [OrderedCommMonoid M] (S : Submonoid M) : OrderedCommMonoid ↥S

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• S.toOrderedCommMonoid = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoid.toLinearOrderedAddCommMonoid {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedAddCommMonoid ↥S

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• S.toLinearOrderedAddCommMonoid = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

instance Submonoid.toLinearOrderedCommMonoid {M : Type u_1} [LinearOrderedCommMonoid M] (S : Submonoid M) : LinearOrderedCommMonoid ↥S

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• S.toLinearOrderedCommMonoid = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [OrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance AddSubmonoid.toOrderedCancelAddCommMonoid {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : OrderedCancelAddCommMonoid ↥S

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• S.toOrderedCancelAddCommMonoid = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toOrderedCancelCommMonoid {M : Type u_1} [OrderedCancelCommMonoid M] (S : Submonoid M) : OrderedCancelCommMonoid ↥S

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• S.toOrderedCancelCommMonoid = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance AddSubmonoid.toLinearOrderedCancelAddCommMonoid {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedCancelAddCommMonoid ↥S

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• S.toLinearOrderedCancelAddCommMonoid = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

instance Submonoid.toLinearOrderedCancelCommMonoid {M : Type u_1} [LinearOrderedCancelCommMonoid M] (S : Submonoid M) : LinearOrderedCancelCommMonoid ↥S

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• S.toLinearOrderedCancelCommMonoid = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.nonneg.proof_1 (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] : ∀ {a b : M}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b

def AddSubmonoid.nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] : AddSubmonoid M

The submonoid of nonnegative elements.

Equations

• AddSubmonoid.nonneg M = { carrier := Set.Ici 0, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddSubmonoid.nonneg.proof_2 (M : Type u_1) [AddMonoid M] [Preorder M] : 0 ≤ 0

@[simp]

theorem Submonoid.oneLE_coe (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] : ↑(Submonoid.oneLE M) = Set.Ici 1

@[simp]

theorem AddSubmonoid.nonneg_coe (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] : ↑(AddSubmonoid.nonneg M) = Set.Ici 0

def Submonoid.oneLE (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] : Submonoid M

The submonoid of elements greater than 1.

Equations

• Submonoid.oneLE M = { carrier := Set.Ici 1, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.mem_nonneg {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} : a ∈ AddSubmonoid.nonneg M ↔ 0 ≤ a

@[simp]

theorem Submonoid.mem_oneLE {M : Type u_1} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} : a ∈ Submonoid.oneLE M ↔ 1 ≤ a

@[simp]

theorem Submonoid.pos_coe (α : Type u_2) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] : ↑(Submonoid.pos α) = Set.Ioi 0

def Submonoid.pos (α : Type u_2) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] : Submonoid α

The submonoid of positive elements.

Equations

• Submonoid.pos α = { carrier := Set.Ioi 0, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem Submonoid.mem_pos {α : Type u_2} [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] {a : α} : a ∈ Submonoid.pos α ↔ 0 < a