exists_familyOfElements — Mathlib

English

There exists a canonical FamilyOfElements associated to the explicit Compatible data hx, namely hx.familyOfElements, which equals x on each i via hx.familyOfElements_ofArrows_mk.

Русский

Существует каноническое семейство элементов, связанное с данными совместимости hx, namely hx.familyOfElements, удовлетворяющее условию hx.familyOfElements_ofArrows_mk.

LaTeX

$$$\exists x' : \mathrm{FamilyOfElements}(P, \mathrm{ofArrows}(X,\pi)), \forall i, x'(\mathrm{ofArrows.mk}\, i) = x_i$$$

Lean4

theorem exists_familyOfElements (hx : Compatible P π x) :
    ∃ (x' : FamilyOfElements P (ofArrows X π)), ∀ (i : I), x' _ (ofArrows.mk i) = x i :=
  by
  choose i h h' using @ofArrows_surj _ _ _ _ _ π
  exact
    ⟨fun Y f hf ↦ P.map (eqToHom (h f hf).symm).op (x _), fun j ↦
      (hx _ j (X j) _ (𝟙 _) <| by rw [← h', id_comp]).trans <| by simp⟩

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