instHasIterationOfShapeElemIic — Mathlib

English

For any J with a linear order and order-theoretic structure, HasIterationOfShape (Set.Iic j).Elem C holds.

Русский

Для любого J с линейным порядком и соответствующей структурой, справедливо HasIterationOfShape (Set.Iic j).Elem C.

LaTeX

$$$\mathrm{HasIterationOfShape}((\mathrm Set.Iic\, j).\mathrm{Elem}, C)$$$

Lean4

instance (j : J) : HasIterationOfShape (Set.Iic j) C :=
  hasIterationOfShape_of_initialSeg C (Set.initialSegIic j)

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