mem_iff — Mathlib

English

A subset p of M is homogeneous with respect to the decomposition if and only if x ∈ p is equivalent to all its coordinates lying in p.

Русский

Подмножество p в M называется однородным по декомпозиции тогда и только тогда, когда элемент x принадлежит p тогда, когда все его координаты лежат в p.

LaTeX

$$DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff ℳ p hp {x} : x ∈ p ↔ ∀ i, (decompose ℳ x i) ∈ p$$

Lean4

theorem mem_iff {P : Type*} [SetLike P M] [AddSubmonoidClass P M] (p : P) (hp : SetLike.IsHomogeneous ℳ p) {x} :
    x ∈ p ↔ ∀ i, (decompose ℳ x i : M) ∈ p := by
  classical
  refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
  rw [← DirectSum.sum_support_decompose ℳ x]
  exact sum_mem (fun i _ ↦ hx i)

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