Theorems · Theorem · category theory

InverseSystem.globalEquiv_naturality

∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : WellFoundedLT ι] [inst_2 : SuccOrder ι] [inst_3 : InverseSystem f]
  (equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x })
  (equivLim : (i : ι) → Order.IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Set.Iio i)), ↑(e x) l = f ⋯ x }) ⦃i j : ι⦄
  (h : i ≤ j) (x : F j),
  (InverseSystem.globalEquiv equivSucc equivLim i) (f h x) =
    InverseSystem.piLTProj h ((InverseSystem.globalEquiv equivSucc equivLim j) x)

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLTSuccOrderInverseSystem