instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported

English

If K is strictly supported with respect to e, then for every degree i the component (K.truncLE'ToRestriction e).f i is an isomorphism.

Русский

Если K строго поддержано относительно e, тогда для каждого уровня i компоненту (K.truncLE'ToRestriction e).f i можно обратить обратной операцией; то есть это изоморфизм.

LaTeX

$$$ \forall i:\iota,\ IsIso\big( (K.truncLE'ToRestriction\ e).f\ i \big) $$$

Lean4

instance [K.IsStrictlySupported e] (i : ι) : IsIso ((K.truncLE'ToRestriction e).f i) :=
  inferInstanceAs (IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop)

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