mem_map — Mathlib

English

Let W be a morphism property on a category C which is stable under transfinite compositions. If h is a transfinite composition of shape J for a morphism f with respect to W, then every step map in the underlying diagram F maps along φ is also in W; i.e., each intermediate morphism h.F.map φ belongs to W for all φ: i → j in the indexing shape J.

Русский

Пусть W — свойство морфизмов в категории C, сохраняющееся под трансфинитной композицией. Если h является трансфинитной композицией формы J по морфизму f относительно W, то каждый промежуточный морфизм в диаграмме F, сопоставляемый через φ: i → j, также принадлежит W; то есть для всех φ: i ⟶ j выполняется W(h.F.map φ).

LaTeX

$$$ \forall i,j \in J\,\forall \phi:\, i \to j,\ W(h.F.map\ \phi).$$

Lean4

theorem mem_map {i j : J} (φ : i ⟶ j) : W (h.F.map φ) :=
  W.transfiniteCompositionsOfShape_le _ _ ((h.iic j).ici ⟨i, leOfHom φ⟩).mem

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