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 (x1 x2 : Fin n.succ) => x1 < x2) s (Fin.cons x₀ x) (Fin.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₁ : (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 (x1 x2 : Fin (n + 1).succ) => x1 < x2) ⇒ r) (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ ((fun (x1 x2 : Fin (n + 1)) => x1 < x2) ⇒ 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 α = { toEquiv := finTwoArrowEquiv α, map_rel_iff' := ⋯ }

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.

Equations

• Fin.consOrderIso α = { toEquiv := Fin.consEquiv α, map_rel_iff' := ⋯ }

@[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)) : (Fin.consOrderIso α) f i = Fin.cons f.1 f.2 i

@[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 (Fin.consOrderIso α)) f = (f 0, Fin.tail f)

@[simp]

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

def Fin.snocOrderIso {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : α (Fin.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.

Equations

• Fin.snocOrderIso α = { toEquiv := Fin.snocEquiv α, map_rel_iff' := ⋯ }

@[simp]

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

@[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 (Fin.snocOrderIso α)) f = (f (Fin.last n), Fin.init f)

@[simp]

theorem Fin.snocOrderIso_toEquiv {n : ℕ} (α : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → LE (α i)] : (Fin.snocOrderIso α).toEquiv = Fin.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.

Equations

• Fin.insertNthOrderIso α p = { toEquiv := Fin.insertNthEquiv α p, map_rel_iff' := ⋯ }

@[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 (Fin.insertNthOrderIso α p)) f = (f p, p.removeNth f)

@[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)) : (Fin.insertNthOrderIso α p) f j = p.insertNth f.1 f.2 j

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.insertNthOrderIso_last (n : ℕ) (α : Type u_2) [LE α] : Fin.insertNthOrderIso (fun (x : Fin (n + 1)) => α) (Fin.last n) = Fin.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.

@[deprecated Fin.insertNthOrderIso]

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 := (Fin.insertNthEquiv α i).symm, 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 = { toEquiv := finSuccAboveEquiv p, 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

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' := ⋯ }

@[simp]

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

@[simp]

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