uniq_symm

Mathlib.CategoryTheory.Localization.Predicate

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.uniq_symm

English

Symmetry of uniq for product: uniq L1 L2 W' has symmetric property with L2,L1.

Русский

Симметрия uniq для произведения: uniq L1 L2 W' симметрична по отношению к L2,L1.

LaTeX

$$$\\text{uniq}\\,L_1 L_2 W'^{\\mathrm{symm}} = \\text{uniq}\\,L_2 L_1 W'^{\\mathrm{symm}}$$$

Lean4

theorem uniq_symm : (uniq L₁ L₂ W').symm = uniq L₂ L₁ W' :=
  by
  dsimp [uniq, Equivalence.trans]
  ext <;> aesop

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

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

Разделы

Аффилиация

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