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, and the lower sets contained in a finset form a finset. In a linear order a lower finset is empty or the initial segment up to its maximum, so the lower finsets are order-isomorphic to WithBot α by their maximum, and a finite chain of n elements has n + 1 of them.

Main definitions

• Fintype.toLocallyFiniteOrderBot: the bottom intervals of a finite order.
• IsLowerSet.orderIsoWithBot: the lower finsets of a linear order as WithBot α.
• Finset.lowerSubsets: the lower sets contained in a finset.

Main results

• IsLowerSet.mem_iff_le_max: a lower finset of a linear order is Iic of its maximum.
• IsLowerSet.eq_empty_or_eq_Iic: a lower finset of a linear order is empty or an Iic.
• Fintype.card_subtype_isLowerSet: a finite chain has one more lower finset than elements.

theorem IsLowerSet.mem_iff_le_max {α : Type u_1} [LinearOrder α] {s : Finset α} {a : α} (h : IsLowerSet ↑s) : a ∈ s ↔ ↑a ≤ s.max

A lower finset of a linear order is the initial segment up to its maximum. [UPSTREAM]

theorem IsLowerSet.subset_or_subset {α : Type u_1} [LinearOrder α] {s t : Finset α} (hs : IsLowerSet ↑s) (ht : IsLowerSet ↑t) : s ⊆ t ∨ t ⊆ s

Lower finsets of a linear order are nested. [UPSTREAM]

@[instance_reducible]

instance instLinearOrderSubtypeFinsetIsLowerSetCoe_linglib {α : Type u_1} [LinearOrder α] : LinearOrder { s : Finset α // IsLowerSet ↑s }

The lower finsets of a linear order form a chain under inclusion. [UPSTREAM]

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Fintype.toLocallyFiniteOrderBot {α : Type u_1} [Preorder α] [Fintype α] [DecidableLT α] [DecidableLE α] : LocallyFiniteOrderBot α

A finite order has finite bottom intervals. This mirrors Fintype.toLocallyFiniteOrder and is not an instance for the same reason. [UPSTREAM]

Equations

• Fintype.toLocallyFiniteOrderBot = { finsetIio := fun (a : α) => {x : α | x < a}, finsetIic := fun (a : α) => {x : α | x ≤ a}, finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }

theorem isLowerSet_coe_empty {α : Type u_1} [LE α] : IsLowerSet ↑∅

theorem isLowerSet_coe_Iic {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] (a : α) : IsLowerSet ↑(Finset.Iic a)

@[simp]

theorem Finset.max_Iic {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] (a : α) : (Iic a).max = ↑a

theorem IsLowerSet.eq_Iic_of_max_eq {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Finset α} {a : α} (h : IsLowerSet ↑s) (ha : s.max = ↑a) : s = Finset.Iic a

A lower finset of a linear order is the initial segment of its maximum.

theorem IsLowerSet.eq_empty_or_eq_Iic {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Finset α} (h : IsLowerSet ↑s) : s = ∅ ∨ ∃ (a : α), s = Finset.Iic a

A lower finset of a linear order is empty or an initial segment.

def IsLowerSet.orderIsoWithBot {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] : { s : Finset α // IsLowerSet ↑s } ≃o WithBot α

The lower finsets of a linear order are WithBot α by their maximum, ∅ going to ⊥ and Iic a to a. [UPSTREAM]

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsLowerSet.orderIsoWithBot_apply {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] (s : { s : Finset α // IsLowerSet ↑s }) : orderIsoWithBot s = (↑s).max

@[simp]

theorem IsLowerSet.orderIsoWithBot_symm_bot {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] : orderIsoWithBot.symm ⊥ = ⟨∅, ⋯⟩

@[simp]

theorem IsLowerSet.orderIsoWithBot_symm_coe {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] (a : α) : orderIsoWithBot.symm ↑a = ⟨Finset.Iic a, ⋯⟩

theorem Fintype.card_subtype_isLowerSet {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [Fintype α] [Fintype { s : Finset α // IsLowerSet ↑s }] : card { s : Finset α // IsLowerSet ↑s } = card α + 1

A finite chain of n elements has n + 1 lower finsets. [UPSTREAM]

@[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 α)

t.lowerSubsets is the finset of 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