range_coe_principal — Mathlib

English

When the filter is principal on a subset S of indices, the range of coe is exactly those x with coordinates in A_i for all i ∈ S.

Русский

Если фильтр является принципиальным на множество S индексов, образ coe равен тем x, у которых x_i ∈ A_i для всех i ∈ S.

LaTeX

$$$\\mathrm{range}(\\mathrm{coe}) = \\{ x : \\prod_i R_i \\;|\\; \\forall i \\in S,\\; x_i \\in A_i \\}.$$$

Lean4

theorem range_coe_principal {S : Set ι} : range ((↑) : Πʳ i, [R i, A i]_[𝓟 S] → Π i, R i) = S.pi A :=
  range_coe R A

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