StrictChains.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteChain.exists_unique_strict_enumeration line 13
Source documentation
Every unordered finite chain has exactly one strictly increasing enumeration.
```
theorem exists_unique_strict_enumeration (s : Finset α) (hs : Ordered s) :
    ∃! l : List α, l.Pairwise (· < ·) ∧ l.toFinset = s := by
…
```
Mentions: OAI.FiniteChain.Ordered
theorem OAI.FiniteChain.ordered_toFinset line 39
Source documentation
Conversely, an actual strictly increasing list gives a finite chain.
```
theorem ordered_toFinset {l : List α} (hl : l.Pairwise (· < ·)) : Ordered l.toFinset := by
…
```
Mentions: OAI.FiniteChain.Ordered
theorem OAI.FiniteChain.full_chain_enumeration line 58
Source documentation
Adding the initial bottom gives a strict chain whose length after bottom equals the cardinality of the nonbottom nodes, including the empty chain.
```
theorem full_chain_enumeration (s : Finset α) (hs : Ordered s)
    (hn : ∀ x ∈ s, x ≠ ⊥) :
    ∃ l : List α, l.toFinset = s ∧ (⊥ :: l).Pairwise (· < ·) ∧ l.length = s.card := by
…
```
Mentions: OAI.FiniteChain.Ordered
def OAI.FiniteChain.StrictChain line 74
Source documentation
The nodes after the initial bottom in a strict chain. The empty list gives the chain containing only bottom.
```
def StrictChain (allowed : α → Prop) :=
…
```
def OAI.FiniteChain.strictToFinset line 77
def OAI.FiniteChain.strictChainEquiv line 84
instance OAI.FiniteChain.strictChainFintype line 109
theorem OAI.FiniteChain.strict_list_weight_eq line 115
Source documentation
Strict enumeration preserves chain length and the signed sum over all chains.
```
theorem strict_list_weight_eq (allowed : α → Prop) :
    (∑ l : StrictChain allowed, (-1 : ℤ)^l.val.length) =
      ∑ s ∈ chains allowed, (-1 : ℤ)^s.card := by
…
```
Mentions: OAI.FiniteChain.StrictChain, OAI.FiniteChain.chains