instance
instPreorderSigmaOfPartialOrder
{ι : Type u_1}
{x : ι → Type u_2}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
:
Equations
- instPreorderSigmaOfPartialOrder = Preorder.mk ⋯ ⋯ ⋯
instance
instPartialOrderSigma
{ι : Type u_1}
{x : ι → Type u_2}
[PartialOrder ι]
[(i : ι) → PartialOrder (x i)]
:
PartialOrder (Sigma x)
Equations
- instPartialOrderSigma = PartialOrder.mk ⋯
theorem
le_of_index_lt
{ι : Type u_1}
{x : ι → Type u_2}
{i j : ι}
{a : x i}
{b : x j}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
(h : i < j)
:
⟨i, a⟩ ≤ ⟨j, b⟩
theorem
lt_of_index_lt
{ι : Type u_1}
{x : ι → Type u_2}
{i j : ι}
{a : x i}
{b : x j}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
(h : i < j)
:
⟨i, a⟩ < ⟨j, b⟩
theorem
index_le_of_le
{ι : Type u_1}
{x : ι → Type u_2}
{i j : ι}
{a : x i}
{b : x j}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
(h : ⟨i, a⟩ ≤ ⟨j, b⟩)
:
i ≤ j
@[simp]
theorem
le_same_index_iff
{ι : Type u_1}
{x : ι → Type u_2}
{i : ι}
{a b : x i}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
:
@[simp]
theorem
lt_same_index_iff
{ι : Type u_1}
{x : ι → Type u_2}
{i : ι}
{a b : x i}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
:
theorem
sigma_order_quotient_iso_index
{ι : Type u_1}
{x : ι → Type u_2}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
[ne : ∀ (i : ι), Nonempty (x i)]
:
IsOrderIso fun (i : ι) =>
Quot.mk (Function.curry (Function.identified_under fun (a : Sigma x) => a.fst)) ⟨i, Classical.choice ⋯⟩
theorem
sum_order_assoc
{ι : Type u_3}
{ι' : ι → Type u_4}
{x : (i : ι) → ι' i → Type u_5}
[PartialOrder ι]
[(i : ι) → PartialOrder (ι' i)]
[(i : ι) → (i' : ι' i) → Preorder (x i i')]
:
IsOrderIso
fun
(x_1 :
(x_1 : Sigma ι') ×
match x_1 with
| ⟨_j, _j'⟩ => x _j _j') =>
match x_1 with
| ⟨⟨i, i'⟩, a⟩ => ⟨i, ⟨i', a⟩⟩
theorem
sum_rightDirected_iff
{ι : Type u_1}
{x : ι → Type u_2}
[PartialOrder ι]
[(i : ι) → Preorder (x i)]
[ne : ∀ (i : ι), Nonempty (x i)]
:
RightDirected (Sigma x) ↔ RightDirected ι ∧ ∀ (i : ι), Maximal i → RightDirected (x i)