rightFractionRel_op_iff

Mathlib.CategoryTheory.Localization.CalculusOfFractions

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

← MathLib Explorer

English

Symmetrically, RightFractionRel z1.op z2.op holds iff LeftFractionRel z1 z2 holds.

Русский

Аналогично, RightFractionRel(z1.op,z2.op) эквивалентно LeftFractionRel(z1,z2).

LaTeX

$$$RightFractionRel(z_1^{op}, z_2^{op}) \iff LeftFractionRel(z_1, z_2)$$$

Lean4

theorem rightFractionRel_op_iff {X Y : C} (z₁ z₂ : W.LeftFraction X Y) :
    RightFractionRel z₁.op z₂.op ↔ LeftFractionRel z₁ z₂ :=
  ⟨fun h => h.unop, fun h => h.op⟩

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

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

Разделы

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

Аффилиация

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