Order properties on tuples

theorem Fin.pi_lex_lt_cons_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} {x₀ y₀ : α 0} {x y : (i : Fin n) → α i.succ} (s : {i : Fin n.succ} → α i → α i → Prop) : Pi.Lex (fun (x1 x2 : Fin n.succ) => x1 < x2) s (cons x₀ x) (cons y₀ y) ↔ s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun (x1 x2 : Fin n) => x1 < x2) (fun (i : Fin n) => s) x y

theorem Fin.insertNth_mem_Icc {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)} {q₁ q₂ : (j : Fin (n + 1)) → α j} : i.insertNth x p ∈ Set.Icc q₁ q₂ ↔ x ∈ Set.Icc (q₁ i) (q₂ i) ∧ p ∈ Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)

theorem Fin.preimage_insertNth_Icc_of_mem {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ q₂ : (j : Fin (n + 1)) → α j} (hx : x ∈ Set.Icc (q₁ i) (q₂ i)) : i.insertNth x ⁻¹' Set.Icc q₁ q₂ = Set.Icc (fun (j : Fin n) => q₁ (i.succAbove j)) fun (j : Fin n) => q₂ (i.succAbove j)

theorem Fin.preimage_insertNth_Icc_of_notMem {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ q₂ : (j : Fin (n + 1)) → α j} (hx : ¬x ∈ Set.Icc (q₁ i) (q₂ i)) : i.insertNth x ⁻¹' Set.Icc q₁ q₂ = ∅

theorem liftFun_vecCons {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α} : Relator.LiftFun (fun (x1 x2 : Fin (n + 1).succ) => x1 < x2) r (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ Relator.LiftFun (fun (x1 x2 : Fin (n + 1)) => x1 < x2) r f f

theorem Fin.liftFun_cons {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin n → α} {a : α} : Relator.LiftFun (fun (x1 x2 : Fin (n + 1)) => x1 < x2) r (cons a f) (cons a f) ↔ (∀ (i : Fin n), r a (f i)) ∧ Relator.LiftFun (fun (x1 x2 : Fin n) => x1 < x2) r f f

theorem Fin.strictMono_insertNth_iff {α : Type u_1} [Preorder α] {n : ℕ} (q : Fin (n + 1)) (x : α) (f : Fin n → α) : StrictMono (q.insertNth x f) ↔ StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i

theorem Fin.strictMono_cons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} {a : α} : StrictMono (cons a f) ↔ (∀ (j : Fin n), a < f j) ∧ StrictMono f

@[simp]

theorem Fin.strictMono_cons_zero_succ {n : ℕ} {f : Fin n → Fin (n + 1)} : StrictMono (cons 0 f) ↔ f = succ

@[simp]

theorem strictMono_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : StrictMono (Matrix.vecCons a f) ↔ a < f 0 ∧ StrictMono f

@[simp]

theorem monotone_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : Monotone (Matrix.vecCons a f) ↔ a ≤ f 0 ∧ Monotone f

@[simp]

theorem monotone_vecEmpty {α : Type u_1} [Preorder α] {a : α} : Monotone ![a]

@[simp]

theorem strictMono_vecEmpty {α : Type u_1} [Preorder α] {a : α} : StrictMono ![a]

@[simp]

theorem strictAnti_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : StrictAnti (Matrix.vecCons a f) ↔ f 0 < a ∧ StrictAnti f

@[simp]

theorem antitone_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : Antitone (Matrix.vecCons a f) ↔ f 0 ≤ a ∧ Antitone f

@[simp]

theorem antitone_vecEmpty {α : Type u_1} [Preorder α] {a : α} : Antitone ![a]

@[simp]

theorem strictAnti_vecEmpty {α : Type u_1} [Preorder α] {a : α} : StrictAnti ![a]

theorem StrictMono.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : StrictMono f) (ha : a < f 0) : StrictMono (Matrix.vecCons a f)

theorem StrictMono.removeNth {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} (hf : StrictMono f) (i : Fin (n + 1)) : StrictMono (i.removeNth f)

theorem StrictAnti.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : StrictAnti f) (ha : f 0 < a) : StrictAnti (Matrix.vecCons a f)

theorem Monotone.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : Monotone f) (ha : a ≤ f 0) : Monotone (Matrix.vecCons a f)

theorem Antitone.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : Antitone f) (ha : f 0 ≤ a) : Antitone (Matrix.vecCons a f)

def OrderIso.piFinTwoIso (α : Fin 2 → Type u_2) [(i : Fin 2) → Preorder (α i)] : ((i : Fin 2) → α i) ≃o α 0 × α 1

Π i : Fin 2, α i is order equivalent to α 0 × α 1. See also OrderIso.finTwoArrowEquiv for a non-dependent version.

def OrderIso.finTwoArrowIso (α : Type u_2) [Preorder α] : (Fin 2 → α) ≃o α × α

The space of functions Fin 2 → α is order equivalent to α × α. See also OrderIso.piFinTwoIso.

def Fin.consOrderIso {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : α 0 × ((i : Fin n) → α i.succ) ≃o ((i : Fin (n + 1)) → α i)

Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the first element of the tuple.

This is Fin.cons as an OrderIso.

@[simp]

theorem Fin.consOrderIso_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i) : (RelIso.symm (consOrderIso α)) f = (f 0, tail f)

@[simp]

theorem Fin.consOrderIso_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : α 0 × ((i : Fin n) → α i.succ)) (i : Fin (n + 1)) : (consOrderIso α) f i = cons f.1 f.2 i

@[simp]

theorem Fin.consOrderIso_toEquiv {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : (consOrderIso α).toEquiv = consEquiv α

def Fin.snocOrderIso {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : α (last n) × ((i : Fin n) → α i.castSucc) ≃o ((i : Fin (n + 1)) → α i)

Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the last element of the tuple.

This is Fin.snoc as an OrderIso.

@[simp]

theorem Fin.snocOrderIso_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : α (last n) × ((i : Fin n) → α i.castSucc)) (i : Fin (n + 1)) : (snocOrderIso α) f i = snoc f.2 f.1 i

@[simp]

theorem Fin.snocOrderIso_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i) : (RelIso.symm (snocOrderIso α)) f = (f (last n), init f)

@[simp]

theorem Fin.snocOrderIso_toEquiv {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : (snocOrderIso α).toEquiv = snocEquiv α

def Fin.insertNthOrderIso {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) : α p × ((i : Fin n) → α (p.succAbove i)) ≃o ((i : Fin (n + 1)) → α i)

Order isomorphism between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple.

This is Fin.insertNth as an OrderIso.

@[simp]

theorem Fin.insertNthOrderIso_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) : (insertNthOrderIso α p) f j = p.insertNth f.1 f.2 j

@[simp]

theorem Fin.insertNthOrderIso_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) : (RelIso.symm (insertNthOrderIso α p)) f = (f p, p.removeNth f)

@[simp]

theorem Fin.insertNthOrderIso_toEquiv {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)) : (insertNthOrderIso α p).toEquiv = insertNthEquiv α p

@[simp]

theorem Fin.insertNthOrderIso_zero {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : insertNthOrderIso α 0 = consOrderIso α

@[simp]

theorem Fin.insertNthOrderIso_last (n : ℕ) (α : Type u_2) [LE α] : insertNthOrderIso (fun (x : Fin (n + 1)) => α) (last n) = snocOrderIso fun (x : Fin (n + 1)) => α

Note this lemma can only be written about non-dependent tuples as insertNth (last n) = snoc is not a definitional equality.

def finSuccAboveOrderIso {n : ℕ} (p : Fin (n + 1)) : Fin n ≃o { x : Fin (n + 1) // x ≠ p }

Fin.succAbove as an order isomorphism between Fin n and {x : Fin (n + 1) // x ≠ p}.

theorem finSuccAboveOrderIso_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (finSuccAboveOrderIso p) i = ⟨p.succAbove i, ⋯⟩

theorem finSuccAboveOrderIso_symm_apply_last {n : ℕ} (x : { x : Fin (n + 1) // x ≠ Fin.last n }) : (finSuccAboveOrderIso (Fin.last n)).symm x = (↑x).castLT ⋯

theorem finSuccAboveOrderIso_symm_apply_ne_last {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x : Fin (n + 1) // x ≠ p }) : (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

def Fin.castLEOrderIso {n m : ℕ} (h : n ≤ m) : Fin n ≃o { i : Fin m // ↑i < n }

Promote a Fin n into a larger Fin m, as a subtype where the underlying values are retained. This is the OrderIso version of Fin.castLE.

@[simp]

theorem Fin.castLEOrderIso_symm_apply {n m : ℕ} (h : n ≤ m) (i : { i : Fin m // ↑i < n }) : (RelIso.symm (castLEOrderIso h)) i = ⟨↑↑i, ⋯⟩

@[simp]

theorem Fin.castLEOrderIso_apply {n m : ℕ} (h : n ≤ m) (i : Fin n) : (castLEOrderIso h) i = ⟨castLE h i, ⋯⟩