Theorems · Theorem · category theory

InverseSystem.isNatEquiv_piEquivSucc

∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [inst_1 : SuccOrder ι]
  {equiv : (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j} {e : F (Order.succ i) ≃ F i × X i} (hi : ¬IsMax i)
  [InverseSystem f],
  (∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x) →
    InverseSystem.IsNatEquiv f equiv → InverseSystem.IsNatEquiv f (InverseSystem.piEquivSucc equiv e hi)

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderSuccOrderInverseSystem