add — Mathlib

English

Adding a single arrow f to a zero-hypercover E, under the covering condition hf, yields a new zero-hypercover with the same underlying data and an updated presieve.

Русский

Добавление стрелки f к нулевому гиперпокрытию E сохраняет базовую структуру и обновляет презивы согласно hf.

LaTeX

$$def add (E : ZeroHypercover J S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J S) : ZeroHypercover J S$$

Lean4

/-- Add a single morphism to a `0`-hypercover. -/
@[simps toPreZeroHypercover]
def add (E : ZeroHypercover.{w} J S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J S) :
    ZeroHypercover.{w} J S where
  __ := E.toPreZeroHypercover.add f
  mem₀ := by rwa [PreZeroHypercover.presieve₀_add]

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