Products of OrderedSub types. #
instance
Prod.orderedSub
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Add α]
[Sub α]
[OrderedSub α]
[Sub β]
[Preorder β]
[Add β]
[OrderedSub β]
:
OrderedSub (α × β)
Equations
- (_ : OrderedSub (α × β)) = (_ : OrderedSub (α × β))
instance
Pi.orderedSub
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
[(i : ι) → Add (α i)]
[(i : ι) → Sub (α i)]
[∀ (i : ι), OrderedSub (α i)]
:
OrderedSub ((i : ι) → α i)
Equations
- (_ : OrderedSub ((i : ι) → α i)) = (_ : OrderedSub ((i : ι) → α i))