collectedBasis_mem — Mathlib

English

Each basis element in the collected basis lies in the corresponding summand A_i.

Русский

Каждый элемент базиса, входящий в собранный базис, принадлежит соответствующему подмодулю A_i.

LaTeX

$$$h.collectedBasis v\ a \in A a.1$$$

Lean4

theorem collectedBasis_mem (h : IsInternal A) {α : ι → Type*} (v : ∀ i, Basis (α i) R (A i)) (a : Σ i, α i) :
    h.collectedBasis v a ∈ A a.1 := by simp

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