one_apply — Mathlib

English

For a principal filter on S, the range of the coordinate evaluation is the set of x with x_i ∈ A_i for all i ∈ S.

Русский

Для принципиального фильтра на S образ координатной оценки состоит из тех x, для которых x_i ∈ A_i для всех i ∈ S.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem one_apply [Π i, One (R i)] [∀ i, OneMemClass (S i) (R i)] (i : ι) : (1 : Πʳ i, [R i, B i]_[𝓕]) i = 1 :=
  rfl

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