The order-convex hull

[UPSTREAM] candidate for Mathlib/Order/UpperLower/Closure.lean: the order-convex hull of a set — the smallest OrdConnected superset — as a bundled ClosureOperator (Set α). It is the order-theoretic twin of convexHull (segment-convexity), built the same way, via ClosureOperator.ofCompletePred over the intersection-closed predicate OrdConnected (Set.ordConnected_sInter).

mathlib already has the characterization ordConnected_iff_upperClosure_inter_lowerClosure and Set.OrdConnected, but not this bundled closure operator. On upstreaming, these declarations move into Mathlib/Order/UpperLower/Closure.lean (next to that characterization) and this file is deleted.

Main declarations

• ordConnectedHull — the order-convex hull as a ClosureOperator (Set α).
• mem_ordConnectedHull — c ∈ ordConnectedHull s ↔ ∃ a b ∈ s, a ≤ c ≤ b.
• ordConnectedHull_eq_upperClosure_inter_lowerClosure — the bridge to upperClosure/lowerClosure.

def ordConnectedHull {α : Type u_1} [Preorder α] : ClosureOperator (Set α)

The order-convex hull of s as a ClosureOperator: the smallest OrdConnected set containing s. The order-theoretic twin of convexHull.

Equations

• ordConnectedHull = ClosureOperator.ofCompletePred Set.OrdConnected ⋯

@[simp]

theorem ordConnectedHull_isClosed {α : Type u_1} [Preorder α] (s : Set α) : ordConnectedHull.IsClosed s = s.OrdConnected

theorem subset_ordConnectedHull {α : Type u_1} [Preorder α] (s : Set α) : s ⊆ ordConnectedHull s

A set is contained in its order-convex hull.

theorem ordConnectedHull_min {α : Type u_1} [Preorder α] {s t : Set α} (h : s ⊆ t) (ht : t.OrdConnected) : ordConnectedHull s ⊆ t

The order-convex hull is the smallest OrdConnected superset.

theorem ordConnectedHull_mono {α : Type u_1} [Preorder α] : Monotone ⇑ordConnectedHull

theorem ordConnected_ordConnectedHull {α : Type u_1} [Preorder α] (s : Set α) : (ordConnectedHull s).OrdConnected

The order-convex hull is OrdConnected.

theorem ordConnectedHull_eq_self {α : Type u_1} [Preorder α] {s : Set α} : ordConnectedHull s = s ↔ s.OrdConnected

A set equals its order-convex hull iff it is OrdConnected.

theorem Set.OrdConnected.ordConnectedHull_eq {α : Type u_1} [Preorder α] {s : Set α} : s.OrdConnected → ordConnectedHull s = s

Alias of the reverse direction of ordConnectedHull_eq_self.

---

A set equals its order-convex hull iff it is OrdConnected.

theorem ordConnectedHull_eq_upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] (s : Set α) : ordConnectedHull s = ↑(upperClosure s) ∩ ↑(lowerClosure s)

The order-convex hull is the intersection of the upper and lower closures.

theorem mem_ordConnectedHull {α : Type u_1} [Preorder α] {s : Set α} {c : α} : c ∈ ordConnectedHull s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≤ c ∧ c ≤ b

Membership in the order-convex hull: the explicit "between two members" form.

@[simp]

theorem ordConnectedHull_empty {α : Type u_1} [Preorder α] : ordConnectedHull ∅ = ∅

@[simp]

theorem ordConnectedHull_univ {α : Type u_1} [Preorder α] : ordConnectedHull Set.univ = Set.univ