instIsStrictlySupportedTruncLE_1 — Mathlib

English

IsIso (K.ιTruncLE e) if and only if K is strictly supported with respect to e.

Русский

Изоморфизм IsIso (K.ιTruncLE e) тогда и только тогда, когда K строго поддержано относительно e.

LaTeX

$$$ \text{IsIso}\big(K.ιTruncLE e\big) \iff K.IsStrictlySupported e $$$

Lean4

instance {ι'' : Type*} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] :
    (K.truncLE e).IsStrictlySupported e' :=
  by
  rw [← isStrictlySupported_op_iff]
  exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e'.op)

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