symm — Mathlib

English

If z1: LeftFraction X Y, z2: LeftFraction Y Z, z3, z3': LeftFraction z1.Y' z2.Y' satisfy a compatibility h3, h3', then z1.comp₀ z2 z3 is related to z1.comp₀ z2 z3' in the LeftFractionRel relation.

Русский

Если z1: LeftFraction X Y, z2: LeftFraction Y Z, z3, z3': LeftFraction z1.Y' z2.Y' удовлетворяют совместимости h3, h3', то связи z1.comp₀ z2 z3 и z1.comp₀ z2 z3' эквивалентны в LeftFractionRel.

LaTeX

$$LeftFractionRel( z1.comp0 z2 z3, z1.comp0 z2 z3' )$$

Lean4

theorem symm {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : LeftFractionRel z₁ z₂) : LeftFractionRel z₂ z₁ :=
  by
  obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
  exact ⟨Z, t₂, t₁, hst.symm, hft.symm, by simpa only [← hst] using ht⟩

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