isInternal_ne_bot_iff — Mathlib

English

For a family A: ι → Submodule R M, the internality of A is equivalent to the internality of its restriction to indices with A_i ≠ ⊥; i.e., IsInternal A ⇔ IsInternal (fun i : { i // A i ≠ ⊥ } ↦ A i).

Русский

Для семейства A : ι → Submodule R M внутренность A эквивалентна внутренности ограничения на те индексы, для которых A_i ≠ ⊥; то есть IsInternal A ⇔ IsInternal (типа {i // A i ≠ ⊥} ↦ A_i).

LaTeX

$$$IsInternal\left(\lambda i: {i // A_i \neq \bot} \mapsto A_i\right) \;\leftrightarrow\; IsInternal A$$$

Lean4

@[simp]
theorem isInternal_ne_bot_iff {A : ι → Submodule R M} : IsInternal (fun i : { i // A i ≠ ⊥ } ↦ A i) ↔ IsInternal A := by
  simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]

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