exists_oneHypercover — Mathlib

English

There exists a hypercover E of X in J with the property that E.sieve0 contains a given S, under the generating condition.

Русский

Существует гиперковер E над X, удовлетворяющий условию включения E.sieve0 в S, при условии генерации.

LaTeX

$$$\\exists E\\;\\exists h\\; E.sieve_0 \\le S$$$

Lean4

theorem exists_oneHypercover [H.IsGenerating] {X : C} (S : Sieve X) (hS : S ∈ J X) :
    ∃ (E : J.OneHypercover X) (_ : H E), E.sieve₀ ≤ S :=
  IsGenerating.le _ hS

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