iff_of_iso

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Square.IsPushout.iff_of_iso

English

For sq1, sq2 with iso e: sq1 ≅ sq2, sq1.IsPushout ↔ sq2.IsPushout.

Русский

Для sq1, sq2 с изоморфизмом e: sq1 ≅ sq2, выполняется sq1.IsPushout ↔ sq2.IsPushout.

LaTeX

$$sq1.IsPushout ↔ sq2.IsPushout$$

Lean4

theorem iff_of_iso {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) : sq₁.IsPushout ↔ sq₂.IsPushout :=
  ⟨fun h ↦ h.of_iso e, fun h ↦ h.of_iso e.symm⟩

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

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

Разделы

Аффилиация

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