presieve₀_sum — Mathlib

English

Same as presieve₀_sum but stated for a variant of PreZeroHypercover; the presieve₀ of the sum is the sup of presieve₀'s.

Русский

То же самое, что и для presieve₀_sum, но для другой версии преднулевого гиперобложки; presieve₀ суммы равна наибольшему верхнему пределу presieve₀.

LaTeX

$$$ (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀ $$$

Lean4

@[simp]
theorem presieve₀_sum : (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀ :=
  by
  rw [presieve₀, presieve₀, presieve₀]
  apply le_antisymm
  · intro Z g ⟨i⟩
    cases i
    · exact Or.inl (.mk _)
    · exact Or.inr (.mk _)
  · rintro Z g (⟨⟨i⟩⟩ | ⟨⟨i⟩⟩)
    · exact ⟨Sum.inl i⟩
    · exact ⟨Sum.inr i⟩

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