English
Define pi(I, p) to be the submodule of dependent functions f(i) ∈ φ(i) such that f(i) ∈ p(i) for all i ∈ I.
Русский
Определим π(I, p) как подпространство зависимых функций f(i) ∈ φ(i), для которых f(i) ∈ p(i) при всех i ∈ I.
LaTeX
$$$$\\pi(I, p) = \\{ f: \\prod_{i} φ(i) \\mid \\forall i\\in I,\\ f(i) ∈ p(i) \\}.$$$$
Lean4
/-- A version of `Set.pi` for submodules. Given an index set `I` and a family of submodules
`p : (i : ι) → Submodule R (φ i)`, `pi I s` is the submodule of dependent functions
`f : (i : ι) → φ i` such that `f i` belongs to `p a` whenever `i ∈ I`. -/
@[simps]
def pi (I : Set ι) (p : (i : ι) → Submodule R (φ i)) : Submodule R ((i : ι) → φ i)
where
carrier := Set.pi I fun i => p i
zero_mem' i _ := (p i).zero_mem
add_mem' {_ _} hx hy i hi := (p i).add_mem (hx i hi) (hy i hi)
smul_mem' c _ hx i hi := (p i).smul_mem c (hx i hi)
