mem₀ — Mathlib

English

Let E be a ZeroHypercover over a precoverage J of S, and suppose E is small. Then the presieve obtained by restricting E to Small is a member of the coverings J S.

Русский

Пусть E — нулевой гиперохват над исходящим покрытием J для S; если E мал, то презив E, ограниченный до Small, принадлежит покрывающим J S.

LaTeX

$$$(E.restrictIndex \\circ Small.restrictFun(E)).presieve_0 \\in J(S)$$$

Lean4

theorem mem₀ (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] :
    (E.restrictIndex <| Small.restrictFun E).presieve₀ ∈ J S :=
  (Small.exists_restrictIndex_mem E).choose_spec.choose_spec

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