Order properties on tuples

theorem Fin.pi_lex_lt_cons_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} {x₀ : α 0} {y₀ : α 0} {x : (i : Fin n) → α i.succ} {y : (i : Fin n) → α i.succ} (s : {i : Fin n.succ} → α i → α i → Prop) : Pi.Lex (fun (x x_1 : Fin n.succ) => x < x_1) s (Fin.cons x₀ x) (Fin.cons y₀ y) ↔ s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun (x x_1 : Fin n) => x < x_1) (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₁ : (j : Fin (n + 1)) → α j} {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₁ : (j : Fin (n + 1)) → α j} {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_not_mem {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i} {q₁ : (j : Fin (n + 1)) → α j} {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 : α} : ((fun (x x_1 : Fin (n + 1).succ) => x < x_1) ⇒ r) (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ ((fun (x x_1 : Fin (n + 1)) => x < x_1) ⇒ r) f f

@[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 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.

Equations

• OrderIso.piFinTwoIso α = { toEquiv := piFinTwoEquiv α, map_rel_iff' := ⋯ }

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

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

Equations

• OrderIso.finTwoArrowIso α = let __src := OrderIso.piFinTwoIso fun (x : Fin 2) => α; { toEquiv := finTwoArrowEquiv α, map_rel_iff' := ⋯ }

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

Order isomorphism between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

Equations

• OrderIso.piFinSuccAboveIso α i = { toEquiv := Equiv.piFinSuccAbove α i, map_rel_iff' := ⋯ }

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}.

Equations

• finSuccAboveOrderIso p = let __spread.0 := finSuccAboveEquiv p; { toEquiv := __spread.0, map_rel_iff' := ⋯ }

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

@[simp]

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

@[simp]

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

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.

Equations

• Fin.castLEOrderIso h = { toFun := fun (i : Fin n) => ⟨Fin.castLE h i, ⋯⟩, invFun := fun (i : { i : Fin m // ↑i < n }) => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }