mem_iff — Mathlib

English

For a homogeneous submodule p, membership is equivalent to membership of every homogeneous component of an element.

Русский

Для однородного подмодуля p принадлежности эквивалентны принадлежности каждой однородной компоненты элемента.

LaTeX

$$$$ {p : Submodule A M} (\mathcal{M} : ι_M \to σ_M) [DecidableEq ι_M] [SetLike σ_M M] [AddSubmonoidClass σ_M M] (hp : p.IsHomogeneous \mathcal{M}) {x} : x \in p \iff \forall i, (decompose \mathcal{M} x i : M) \in p. $$$$

Lean4

theorem mem_iff {p : Submodule A M} (ℳ : ιM → σM) [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M]
    [Decomposition ℳ] (hp : p.IsHomogeneous ℳ) {x} : x ∈ p ↔ ∀ i, (decompose ℳ x i : M) ∈ p :=
  AddSubmonoidClass.IsHomogeneous.mem_iff ℳ _ hp

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