presieve₀_add — Mathlib

English

The presieve₀ of the added hypercover E.add f equals the sup of E.presieve₀ and the singleton generated by f.

Русский

Presieve₀ добавления гиперобложки E.add f равен сумме (супремуму) presieve₀ E и одноэлементного сингуляра f.

LaTeX

$$$ (E.add f).presieve₀ = E.presieve₀ ⊔ .singleton f $$$

Lean4

@[simp]
theorem presieve₀_add {T : C} (f : T ⟶ S) : (E.add f).presieve₀ = E.presieve₀ ⊔ .singleton f := by
  simp [add, presieve₀_reindex, presieve₀_sum]

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