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