Lower sets carried by finsets

The lower-set predicate on the coercion of a finset, IsLowerSet (↑s : Set α), is decidable over a finite type with decidable order — the [UPSTREAM] candidate here — and the lower sets contained in a finset form a finset, closed under removing an element together with everything above it.

Main declarations

• Finset.lowerSubsets — the lower sets contained in a finset.
• Finset.filter_not_le_mem_lowerSubsets — removing an upper cone stays inside.

@[instance_reducible]

instance instDecidableIsLowerSetCoeFinset_linglib {α : Type u_1} [Preorder α] [Fintype α] [DecidableEq α] [DecidableLE α] (s : Finset α) : Decidable (IsLowerSet ↑s)

Equations

• instDecidableIsLowerSetCoeFinset_linglib s = decidable_of_iff (∀ a ∈ s, ∀ b ≤ a, b ∈ s) ⋯

def Finset.lowerSubsets {α : Type u_1} [Preorder α] [Fintype α] [DecidableEq α] [DecidableLE α] (t : Finset α) : Finset (Finset α)

The lower sets contained in t.

Equations

• t.lowerSubsets = {s ∈ t.powerset | IsLowerSet ↑s}

@[simp]

theorem Finset.mem_lowerSubsets {α : Type u_1} [Preorder α] [Fintype α] [DecidableEq α] [DecidableLE α] {s t : Finset α} : s ∈ t.lowerSubsets ↔ s ⊆ t ∧ IsLowerSet ↑s

theorem Finset.filter_not_le_mem_lowerSubsets {α : Type u_1} [Preorder α] [Fintype α] [DecidableEq α] [DecidableLE α] {s t : Finset α} (h : s ∈ t.lowerSubsets) (a : α) : {b ∈ s | ¬a ≤ b} ∈ t.lowerSubsets