Chains of covers

This file proves a discrete intermediate value property. A list in which each element is weakly covered by the next moves up a linear order one step at a time, so it cannot pass over a value. The file also decides the covering relations on a finite order, which mathlib does only for Bool. [UPSTREAM]

Main results

• List.IsChain.mem_of_le_of_le: a chain of weak covers that starts at or below x and reaches an element at or above x contains x.

@[instance_reducible]

instance WCovBy.instDecidableRelOfFintype {α : Type u_1} [Fintype α] [Preorder α] [DecidableLE α] [DecidableLT α] : DecidableRel fun (x1 x2 : α) => x1 ⩿ x2

Equations

• WCovBy.instDecidableRelOfFintype a b = decidable_of_iff (a ≤ b ∧ ∀ (c : α), a < c → ¬c < b) ⋯

@[instance_reducible]

instance CovBy.instDecidableRelOfFintype {α : Type u_1} [Fintype α] [Preorder α] [DecidableLT α] : DecidableRel fun (x1 x2 : α) => x1 ⋖ x2

Equations

• CovBy.instDecidableRelOfFintype a b = decidable_of_iff (a < b ∧ ∀ (c : α), a < c → ¬c < b) ⋯

theorem List.IsChain.mem_of_le_of_le {α : Type u_1} [LinearOrder α] {x m a : α} {l : List α} : IsChain (fun (x1 x2 : α) => x1 ⩿ x2) (a :: l) → a ≤ x → m ∈ a :: l → x ≤ m → x ∈ a :: l

A chain of weak covers that starts at or below x and reaches an element at or above x contains x.