English
Let C be a category and J a poset. If F : J → C is a diagram which is well–order continuous and J′ ⊆ J is an initial segment (i.e., the inclusion J′ ↪ J preserves the order and initial prefix property), then the restricted diagram F|_{J′} : J′ → C is again well–order continuous.
Русский
Пусть C – категория, J – частично упорядоченное множество. Если F: J → C – диаграмма, которая удовлетворяет свойству непрерывности по хорошо упорядоченным линейкам (IsWellOrderContinuous), и J′ ⊆ J является начальным отрезком, то ограниченная диаграмма F|_{J′}: J′ → C также имеет свойство IsWellOrderContinuous.
LaTeX
$$$\\operatorname{IsWellOrderContinuous}(F) \\wedge f : J' \\le_i J \\Rightarrow \\operatorname{IsWellOrderContinuous}(F \\circ f) $$$
Lean4
instance (F : J ⥤ C) {J' : Type w'} [PartialOrder J'] (f : J' ≤i J) [F.IsWellOrderContinuous] :
(f.monotone.functor ⋙ F).IsWellOrderContinuous where
nonempty_isColimit m'
hm' := ⟨F.isColimitOfIsWellOrderContinuous' ((Set.principalSegIio m').transInitial f) (by simpa)⟩
