pairwiseToOpensLeCoverObj — Mathlib

English

The sheaf condition in OpensLeCover is equivalent to the sheaf condition in PairwiseIntersections.

Русский

УсловиеSheaf для OpensLeCover эквивалентно условиюSheaf для PairwiseIntersections.

LaTeX

$$$F.IsSheafOpensLeCover \iff F.IsSheafPairwiseIntersections$$$

Lean4

/-- Implementation detail:
the object level of `pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U`
-/
@[simp]
def pairwiseToOpensLeCoverObj : Pairwise ι → OpensLeCover U
  | single i => ⟨U i, ⟨i, le_rfl⟩⟩
  | Pairwise.pair i j => ⟨U i ⊓ U j, ⟨i, inf_le_left⟩⟩

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