ab_exact_iff_function_exact

Mathlib.Algebra.Homology.ShortComplex.Ab

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.ab_exact_iff_function_exact

Lean4

theorem ab_exact_iff_function_exact : S.Exact ↔ Function.Exact S.f S.g :=
  by
  rw [S.ab_exact_iff]
  apply forall_congr'
  intro x₂
  constructor
  · intro h
    refine ⟨h, ?_⟩
    rintro ⟨x₁, rfl⟩
    simp only [ab_zero_apply]
  · tauto

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

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

Разделы

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

Аффилиация

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