SetoidRestrict.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.card_quotient_split line 17

Source documentation

Restricting an equivalence relation to an invariant part and its complement partitions its actual quotient, not merely its representatives.

theorem card_quotient_split [Finite D] (s : Setoid D) (P : D → Prop)
    (hP : ∀ {x y}, s x y → (P x ↔ P y)) :
    Nat.card (Quotient s) =
      Nat.card (Quotient (s.comap (Subtype.val : Subtype P → D))) +
      Nat.card (Quotient (s.comap (Subtype.val : {x : D // ¬ P x} → D))) := by
…

theorem OAI.HyperbolicObstruction.PictureSwitch.comap_sup_of_invariant line 35

Source documentation

For invariant subsets, taking the join of equivalence relations commutes with restriction. The invariant hypothesis is essential.

theorem comap_sup_of_invariant (r s : Setoid D) (P : D → Prop)
    (hr : ∀ {x y}, r x y → (P x ↔ P y))
    (hs : ∀ {x y}, s x y → (P x ↔ P y)) :
    (r ⊔ s).comap (Subtype.val : Subtype P → D) =
      r.comap Subtype.val ⊔ s.comap Subtype.val := by
…