instIsWellOrderContinuousCompFunctorEquivalence

English

Let F : J → C be a diagram which is IsWellOrderContinuous, and let e : J′ ≃o J be an order isomorphism. Then the reindexed diagram F ∘ e is IsWellOrderContinuous.

Русский

Пусть F: J → C является диаграммой с IsWellOrderContinuous, и пусть e : J′ ≃o J — упорядоченная изоморфия. Тогда переиндексация диаграммы F по e, то есть F ∘ e, имеет IsWellOrderContinuous.

LaTeX

$$$\\operatorname{IsWellOrderContinuous}(F) \\Rightarrow \\operatorname{IsWellOrderContinuous}(F \\circ e)$ where $e : J' \\simeq_o J$.$$

Lean4

instance (F : J ⥤ C) {J' : Type w'} [PartialOrder J'] (e : J' ≃o J) [F.IsWellOrderContinuous] :
    (e.equivalence.functor ⋙ F).IsWellOrderContinuous :=
  inferInstanceAs (e.toInitialSeg.monotone.functor ⋙ F).IsWellOrderContinuous

Похожие утверждения