family_of_elements_compatible — Mathlib

English

For U in Cᵒᵖ and s ∈ F.obj U, the familyOfElementsOfSection s is compatible.

Русский

Для U ∈ Cᵒᵖ и s ∈ F.obj U, семейство элементов раздела совместимо.

LaTeX

$$$ (G.familyOfElementsOfSection s).Compatible $$$

Lean4

theorem family_of_elements_compatible {U : Cᵒᵖ} (s : F.obj U) : (G.familyOfElementsOfSection s).Compatible :=
  by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e
  refine
    Subtype.ext
      ?_ -- Porting note: `ext1` does not work here

  change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
  rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, e]

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