homOfIndex — Mathlib

English

The dependent pair corresponding to an index i is mapped to the open U_i and its inclusion data.

Русский

Пара зависимости, соответствующая индексу i, отображается на открытое множество U_i и данные вложения.

LaTeX

$$$\\mathrm{homOfIndex}(i) = (U_i, \\; i, \\; \\text{proof})$$$

Lean4

/-- An index `i : ι` can be turned into a dependent pair `(V, f)`, where `V` is an open set and
`f : V ⟶ iSup U` is a member of `presieveOfCovering U f`.
-/
def homOfIndex (i : ι) : Σ V, { f : V ⟶ iSup U // presieveOfCovering U f } :=
  ⟨U i, Opens.leSupr U i, i, rfl⟩

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