coe_iInf

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.coe_iInf

English

The underlying set of the indexed infimum equals the intersection of the images of the sets.

Русский

Основание инфимума по индексу совпадает с пересечением образов множеств.

LaTeX

$$$ \\mathrm{coe}\\, (iInf i, S_i) = \\bigcap_i \\mathrm{coe}(S_i)$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} : (↑(⨅ i, S i) : Set A) = ⋂ i, S i := by simp [iInf]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru