condition — Mathlib

English

The value of P.map along a morphism on a leg of a cover matches via the base relation of the pullback.

Русский

Значение P.map вдоль морфизма по ножке покрытия соответствует базовой связи вытяжки.

LaTeX

$$$P.map I.r.g_1.op (x (S.shape.fst I)) = P.map I.r.g_2.op (x (S.shape.snd I))$$$

Lean4

theorem condition {X} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) (I : S.Relation) :
    P.map I.r.g₁.op (x (S.shape.fst I)) = P.map I.r.g₂.op (x (S.shape.snd I)) :=
  x.2 _

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