iff

Mathlib.CategoryTheory.Shift.Localization

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff

Lean4

theorem iff {X Y : C} (f : X ⟶ Y) (a : A) : W (f⟦a⟧') ↔ W f :=
  by
  conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]
  rfl

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

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

Разделы

Аффилиация

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