Order-connected finite sets are closed intervals #
[UPSTREAM] candidate for Mathlib/Order/Interval/Finset/Basic.lean: an order-connected finset
of a locally finite linear order that contains the top element is the closed interval from its
least element up to the top, and an order-connected set containing the top is an upper set. This
is the shape of a "contiguous segment of a hierarchy" wherever a linguistic scale is linearly
ordered and a strategy covers a run of it.
Main statements #
Finset.eq_Icc_top_of_ordConnected_coe: with the top element in the set, the interval reaches it.Set.OrdConnected.isUpperSet_of_top_mem: an order-connected set containing the top element is an upper set.
theorem
Set.OrdConnected.isUpperSet_of_top_mem
{α : Type u_1}
[Preorder α]
[OrderTop α]
{s : Set α}
(hs : s.OrdConnected)
(ht : ⊤ ∈ s)
:
IsUpperSet s
An order-connected set containing the top element is an upper set.
@[instance_reducible]
instance
Finset.decidableOrdConnectedCoe
{α : Type u_1}
[Preorder α]
[DecidableEq α]
[LocallyFiniteOrder α]
(s : Finset α)
:
Decidable (↑s).OrdConnected
Order-connectedness of a finset is decided on its closed intervals.
Equations
- s.decidableOrdConnectedCoe = decidable_of_iff (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ Finset.Icc x y, z ∈ s) ⋯
theorem
Finset.eq_Icc_top_of_ordConnected_coe
{α : Type u_1}
[LinearOrder α]
[LocallyFiniteOrder α]
{s : Finset α}
[OrderTop α]
(hc : (↑s).OrdConnected)
(ht : ⊤ ∈ s)
:
s = Icc (s.min' ⋯) ⊤
An order-connected finset containing the top element is the closed interval from its least element up to the top.