Complete linear order instance on lexicographically ordered pi types

We show that for α a family of complete linear orders, the lexicographically ordered type of dependent functions Πₗ i, α i is itself a complete linear order.

Lexicographic ordering

instance Pi.Lex.instInfSetLexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] : InfSet (Lex ((i : ι) → (fun (i : ι) => α i) i))

theorem Pi.Lex.sInf_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))) (i : ι) : sInf s i = ⨅ (e : ↑{e : Lex ((i : ι) → (fun (i : ι) => α i) i) | e ∈ s ∧ ∀ j < i, e j = sInf s j}), ↑e i

theorem Pi.Lex.sInf_apply_le {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))} {i : ι} {e : Lex ((i : ι) → (fun (i : ι) => α i) i)} (he : e ∈ s) (h : ∀ j < i, e j = sInf s j) : sInf s i ≤ e i

theorem Pi.Lex.le_sInf_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))} {i : ι} {e : Lex ((i : ι) → (fun (i : ι) => α i) i)} (h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i) : e i ≤ sInf s i

instance Pi.Lex.instSupSetLexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] : SupSet (Lex ((i : ι) → (fun (i : ι) => α i) i))

theorem Pi.Lex.sSup_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))) (i : ι) : sSup s i = ⨆ (e : ↑{e : Lex ((i : ι) → (fun (i : ι) => α i) i) | e ∈ s ∧ ∀ j < i, e j = sSup s j}), ↑e i

theorem Pi.Lex.le_sSup_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))} {i : ι} {e : Lex ((i : ι) → (fun (i : ι) => α i) i)} (he : e ∈ s) (h : ∀ j < i, e j = sSup s j) : e i ≤ sSup s i

theorem Pi.Lex.sSup_apply_le {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun (i : ι) => α i) i))} {i : ι} {e : Lex ((i : ι) → (fun (i : ι) => α i) i)} (h : ∀ f ∈ s, (∀ j < i, f j = sSup s j) → f i ≤ e i) : sSup s i ≤ e i

noncomputable instance Pi.Lex.completeLattice {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] : CompleteLattice (Lex ((i : ι) → (fun (i : ι) => α i) i))

noncomputable instance Pi.Lex.instCompleteLinearOrderLexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedLT ι] : CompleteLinearOrder (Lex ((i : ι) → (fun (i : ι) => α i) i))

Colexicographic ordering

instance Pi.Colex.instInfSetColexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] : InfSet (Colex ((i : ι) → α i))

theorem Pi.Colex.sInf_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] (s : Set (Colex ((i : ι) → α i))) (i : ι) : sInf s i = ⨅ (e : ↑{e : Colex ((i : ι) → α i) | e ∈ s ∧ ∀ j > i, e j = sInf s j}), ↑e i

theorem Pi.Colex.sInf_apply_le {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)} (he : e ∈ s) (h : ∀ j > i, e j = sInf s j) : sInf s i ≤ e i

theorem Pi.Colex.le_sInf_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)} (h : ∀ f ∈ s, (∀ j > i, f j = sInf s j) → e i ≤ f i) : e i ≤ sInf s i

instance Pi.Colex.instSupSetColexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] : SupSet (Colex ((i : ι) → α i))

theorem Pi.Colex.sSup_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] (s : Set (Colex ((i : ι) → α i))) (i : ι) : sSup s i = ⨆ (e : ↑{e : Colex ((i : ι) → α i) | e ∈ s ∧ ∀ j > i, e j = sSup s j}), ↑e i

theorem Pi.Colex.le_sSup_apply {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)} (he : e ∈ s) (h : ∀ j > i, e j = sSup s j) : e i ≤ sSup s i

theorem Pi.Colex.sSup_apply_le {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)} (h : ∀ f ∈ s, (∀ j > i, f j = sSup s j) → f i ≤ e i) : sSup s i ≤ e i

noncomputable instance Pi.Colex.completeLattice {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] : CompleteLattice (Colex ((i : ι) → α i))

noncomputable instance Pi.Colex.instCompleteLinearOrderColexForall {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CompleteLinearOrder (α i)] [WellFoundedGT ι] : CompleteLinearOrder (Colex ((i : ι) → α i))