ChainToggle.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The alternating sum of finite chains cancels when an admissibility condition is stable under joining with a fixed nonbottom element. The involution inserts or removes the join of that element with the largest chain element that does not lie above it. Bottom is implicit, so an empty set represents the chain consisting of bottom alone and has sign +1.

def OAI.FiniteChain.Ordered line 18
Source documentation
Every pair of members of a finite set is comparable.
```
def Ordered (s : Finset α) : Prop := ∀ a ∈ s, ∀ b ∈ s, a ≤ b ∨ b ≤ a
…
```
theorem OAI.FiniteChain.sup_bot_or_mem line 21
def OAI.FiniteChain.bad line 37
Source documentation
The chain elements which do not lie above the fixed element.
```
noncomputable def bad (P : α) (s : Finset α) : Finset α := by
…
```
def OAI.FiniteChain.pivot line 41
Source documentation
The largest element of bad P s, or bottom if there are none.
```
noncomputable def pivot (P : α) (s : Finset α) : α := (bad P s).sup id
```
Mentions: OAI.FiniteChain.bad
def OAI.FiniteChain.inserted line 43
Source documentation
The element whose presence in the chain is toggled.
```
noncomputable def inserted (P : α) (s : Finset α) : α := pivot P s ⊔ P
```
Mentions: OAI.FiniteChain.pivot
def OAI.FiniteChain.toggle line 45
Source documentation
Insert or remove the join of the pivot with the fixed element.
```
noncomputable def toggle (P : α) (s : Finset α) : Finset α := by
…
```
theorem OAI.FiniteChain.pivot_description line 50
theorem OAI.FiniteChain.comparable_inserted line 62
theorem OAI.FiniteChain.bad_toggle line 78
theorem OAI.FiniteChain.toggle_twice line 90
def OAI.FiniteChain.Admissible line 99
Source documentation
A chain of nonbottom elements satisfying the admissibility condition.
```
def Admissible (allowed : α → Prop) (s : Finset α) : Prop :=
…
```
def OAI.FiniteChain.chains line 102
Source documentation
The finite set of admissible chains.
```
noncomputable def chains (allowed : α → Prop) : Finset (Finset α) := by
…
```
theorem OAI.FiniteChain.toggle_admissible line 107

theorem OAI.FiniteChain.alternating_chain_sum_zero line 139

Source documentation

A join-stable class of chains has vanishing alternating sum.

theorem alternating_chain_sum_zero {allowed : α → Prop} {P : α} (hP : P ≠ ⊥)
    (hbot : allowed ⊥) (hjoin : ∀ q, allowed q → allowed (q ⊔ P)) :
    ∑ s ∈ chains allowed, (-1 : ℤ) ^ s.card = 0 := by
…

Mentions: OAI.FiniteChain.chains