trunc — Mathlib

English

The trunc operation on an iteration yields a smaller index j′ with a restricted F such that iter maps agree via congruence maps.

Русский

Обрезание (trunc) итерации даёт меньший индекс j′ и ограниченное F, при этом отображения согласованы по гомоморфизмам.

LaTeX

$$$ \\text{trunc} : (iter : Φ.Iteration j) \\to (iter' : Φ.Iteration j') $$$

Lean4

/-- The element in `Φ.Iteration i` that is deduced from an element
in `Φ.Iteration j` when `i ≤ j`. -/
@[simps F]
def trunc (iter : Φ.Iteration j) {j' : J} (hj' : j' ≤ j) : Φ.Iteration j'
    where
  F := restrictionLE iter.F hj'
  obj_bot := iter.obj_bot
  arrowSucc_eq i hi := iter.arrowSucc_eq i (lt_of_lt_of_le hi hj')
  arrowMap_limit i hi hij k hk := iter.arrowMap_limit i hi (hij.trans hj') k hk

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