ofLE — Mathlib

English

If W ≤ W' and h is a transfinite composition of shape J in W, then h is also a transfinite composition of shape J in W'.

Русский

Если W ⊆ W' и h является трансфинитной композицией формы J через W, то она же остается трансфинитной композицией формы J через W'.

LaTeX

$$$hW : W.TransfiniteCompositionOfShape J f \Rightarrow hW' : W'.TransfiniteCompositionOfShape J f \text{ от указанного включения } W \le W'$$$

Lean4

/-- If `W ≤ W'`, then transfinite compositions of shape `J` of morphisms in `W`
are also transfinite composition of shape `J` of morphisms in `W'`. -/
@[simps toTransfiniteCompositionOfShape]
def ofLE {W' : MorphismProperty C} (hW : W ≤ W') : W'.TransfiniteCompositionOfShape J f
    where
  __ := h.toTransfiniteCompositionOfShape
  map_mem j hj := hW _ (h.map_mem j hj)

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