Theorems · Definition · category theory

InverseSystem.PEquivOn.casesOn

{ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [inst_1 : SuccOrder ι] →
            {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
              {s : Set ι} →
                {motive : InverseSystem.PEquivOn f equivSucc s → Sort u} →
                  (t : InverseSystem.PEquivOn f equivSucc s) →
                    ((equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i) →
                        (nat : InverseSystem.IsNatEquiv f equiv) →
                          (compat :
                              ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
                                (equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2) →
                            motive { equiv := equiv, nat := nat, compat := compat }) →
                      motive t

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderSuccOrder