range_structureMap — Mathlib

English

The range of the structure map 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})(R,A,𝓕) = \\{ f : \\text{RestrictedProduct} \\mid \\forall i, f.1(i) \\in A_i \\}.$$$

Lean4

theorem range_structureMap : Set.range (structureMap R A 𝓕) = {f | ∀ i, f.1 i ∈ A i} :=
  subset_antisymm (range_subset_iff.mpr fun x i ↦ (x i).2)
    (fun _ hx ↦ mem_range.mpr <| exists_structureMap_eq_of_forall R A hx)

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