instSmallOfSmallI₀ — Mathlib

English

If J is a precover and S is an object of C, then any zero hypercover E over S whose indexing set I0 is small can be equipped with a Small structure; i.e., E admits a small presentation compatible with the indexing.

Русский

Если J задаёт покрытие, а S — объект категории C, то любой нулевой гиперпокрытие E над S с малым индексным множеством I₀ можно представить как малый; то есть у E есть соответствующая малость.

LaTeX

$$$[Small(E.I_0)] \\Rightarrow ZeroHypercover.Small(E)$$$

Lean4

instance (E : ZeroHypercover.{w} J S) [Small.{w'} E.I₀] : ZeroHypercover.Small.{w'} E where
  exists_restrictIndex_mem := ⟨_, (equivShrink E.I₀).symm, by simp [E.mem₀]⟩

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