mem_incl_app — Mathlib

English

Let W be a transfinite composition property as above. Then for every index j in J, the j-th inclusion map h.incl.app j belongs to W.

Русский

Пусть W — трансфинитное свойство композиции; тогда для каждого j ∈ J включение h.incl.app j принадлежит W.

LaTeX

$$$ \forall j:\, J,\ W(h.incl.app j).$$

Lean4

theorem mem_incl_app (j : J) : W (h.incl.app j) :=
  W.transfiniteCompositionsOfShape_le _ _ (h.ici j).mem

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