isIso_ιTruncLE_iff

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.isIso_ιTruncLE_iff

← MathLib Explorer

English

IsIso (K.ιTruncLE e) iff K is strictly supported with respect to e.

Русский

IsIso (K.ιTruncLE e) эквивалентно K строго поддержано относительно e.

LaTeX

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

Lean4

theorem isIso_ιTruncLE_iff : IsIso (K.ιTruncLE e) ↔ K.IsStrictlySupported e :=
  ⟨fun _ ↦ isStrictlySupported_of_iso (asIso (K.ιTruncLE e)) e, fun _ ↦ inferInstance⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru