coe_pi — Mathlib

English

Let I be a set of indices and for every i a submonoid S_i of M_i. The pi- construction collects functions f: ∀ i, M_i such that f(i) ∈ S_i for all i ∈ I. Then the set of all such functions is exactly Set.pi I (S i).

Русский

Пусть I — множество индексов, для каждого i дано подмножество-подмоноид S_i ⊆ M_i. Конструкция π по I собирает функции f: ∀ i, M_i такие, что f(i) ∈ S_i для всех i из I. Тогда множество таких функций равно Set.pi I (S i).

LaTeX

$$$ (\pi I S : Set (∀ i, M i)) = Set.pi I (fun i => (S i : Set (M i))) $$$

Lean4

@[to_additive]
theorem coe_pi (I : Set ι) (S : ∀ i, Submonoid (M i)) :
    (pi I S : Set (∀ i, M i)) = Set.pi I fun i => (S i : Set (M i)) :=
  rfl

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