English
A submonoid is either the bottom submonoid or there exists a non-identity element.
Русский
Подмножество либо равно ⊥, либо существует неединичный элемент.
LaTeX
$$$ \text{bot\_or\_exists\_ne\_one} (S) : S = \bot \lor \exists x \in S, x \neq 1_M$$$
Lean4
/-- A version of `Set.pi` for submonoids. Given an index set `I` and a family of submodules
`s : Π i, Submonoid f i`, `pi I s` is the submonoid of dependent functions `f : Π i, f i` such that
`f i` belongs to `Pi I s` whenever `i ∈ I`. -/
@[to_additive /-- A version of `Set.pi` for `AddSubmonoid`s. Given an index set `I` and a family
of submodules `s : Π i, AddSubmonoid f i`, `pi I s` is the `AddSubmonoid` of dependent functions
`f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`. -/
]
def pi (I : Set ι) (S : ∀ i, Submonoid (M i)) : Submonoid (∀ i, M i)
where
carrier := I.pi fun i => (S i).carrier
one_mem' i _ := (S i).one_mem
mul_mem' hp hq i hI := (S i).mul_mem (hp i hI) (hq i hI)
