X_mem_supported — Mathlib

English

For a nontrivial R, X_i belongs to the subalgebra supported on s if and only if i ∈ s.

Русский

Для не тривиального кольца R верно: X_i принадлежит подалгебре, поддерживаемой на s тогда и только тогда, когда i ∈ s.

LaTeX

$$$$ X_i \in \mathrm{supported}(R,s) \iff i \in s \quad [\text{Nontrivial }R] $$$$

Lean4

@[simp]
theorem X_mem_supported [Nontrivial R] {i : σ} : X i ∈ supported R s ↔ i ∈ s := by simp [mem_supported]

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