structureMap — Mathlib

English

The range of structureMap consists of all elements whose i-th projection lies in A_i for every i.

Русский

Образ structureMap состоит из всех элементов, для которых i-й проекции принадлежит A_i для каждого i.

LaTeX

$$$\\mathrm{range}(\\mathrm{structureMap}) = \\{ f \\in \\mathrm{RestrictedProduct}(R_i, A_i, 𝓕) \\mid \\forall i, f.1(i) \\in A_i \\}.$$$

Lean4

/-- The *structure map* of the restricted product is the obvious inclusion from `Π i, A i`
into `Πʳ i, [R i, A i]_[𝓕]`. -/
def structureMap (x : Π i, A i) : Πʳ i, [R i, A i]_[𝓕] :=
  ⟨fun i ↦ x i, .of_forall fun i ↦ (x i).2⟩

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