QuotientSum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.quotientSplitEquiv line 16

Source documentation

Exact class decomposition under an invariant predicate.

def quotientSplitEquiv (s : Setoid D) (P : D → Prop)
    (hP : ∀ {x y}, s x y → (P x ↔ P y)) :
    Quotient (s.comap (Subtype.val : Subtype P → D)) ⊕
      Quotient (s.comap (Subtype.val : {x : D // ¬ P x} → D)) ≃ Quotient s := by
…

lemma OAI.HyperbolicObstruction.PictureSwitch.quotientSplitEquiv_inl line 28
lemma OAI.HyperbolicObstruction.PictureSwitch.quotientSplitEquiv_inr line 32
def OAI.HyperbolicObstruction.PictureSwitch.classSum line 39
Source documentation
Sum of a weight ONCE per actual equivalence class.
```
def classSum (s : Setoid D) (w : D → A) (hw : s ≤ Setoid.ker w) : A := by
…
```

theorem OAI.HyperbolicObstruction.PictureSwitch.classSum_split line 44

Source documentation

Restriction partitions the exact sum of class weights.

theorem classSum_split (s : Setoid D) (w : D → A) (hw : s ≤ Setoid.ker w)
    (P : D → Prop) (hP : ∀ {x y}, s x y → (P x ↔ P y)) :
    classSum s w hw =
      classSum (s.comap (Subtype.val : Subtype P → D)) (w ∘ Subtype.val) (fun _ _ h => hw h) +
      classSum (s.comap (Subtype.val : {x : D // ¬ P x} → D)) (w ∘ Subtype.val) (fun _ _ h => hw h) := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.classSum