pairwiseToOpensLeCoverMap — Mathlib

English

The limit of the OpensLeCover diagram is equivalent to the limit of the Pairwise diagram via the pairwise-cocone equivalence.

Русский

Предел диаграммы OpensLeCover эквивалентен пределу диаграммы Pairwise через эквивалентность кокона.

LaTeX

$$$\text{IsLimit}(\text{opensLeCoverCocone}) \approx \text{IsLimit}(\text{pairwise diagram})$$$

Lean4

/-- Implementation detail:
the morphism level of `pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U`
-/
def pairwiseToOpensLeCoverMap :
    ∀ {V W : Pairwise ι}, (V ⟶ W) → (pairwiseToOpensLeCoverObj U V ⟶ pairwiseToOpensLeCoverObj U W)
  | _, _, id_single _ => 𝟙 _
  | _, _, id_pair _ _ => 𝟙 _
  | _, _, left _ _ => homOfLE inf_le_left
  | _, _, right _ _ => homOfLE inf_le_right

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