familyOfElements_isCompatible — Mathlib

English

There exists a unique section lifting a compatible family across a cover, by the previous constructive argument.

Русский

Существет уникальный раздел, поднимающий совместимую семью через покрытие, получаемый ранее.

LaTeX

$$$\\exists! s \\in F.\\text{sections}, \\forall i, s(Y_i)=x_i$$$

Lean4

theorem familyOfElements_isCompatible (hx : x.IsCompatible) (X : C) : (familyOfElements x X).Compatible :=
  by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ ⟨i₁, ⟨φ₁⟩⟩ ⟨i₂, ⟨φ₂⟩⟩ _
  simpa [hx.familyOfElements_apply f₁ i₁ φ₁, hx.familyOfElements_apply f₂ i₂ φ₂] using hx Z i₁ i₂ (g₁ ≫ φ₁) (g₂ ≫ φ₂)

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