coe_iInf — Mathlib

English

The underlying set of the infimum of a family of Subalgebras equals the intersection of all members: ↑(iInf S) = ⋂ i, ↑(S i).

Русский

Основное множество пересечения множества подпалгебр равно пересечению всех элементов: ↑(iInf S) = ⋂ i, ↑(S i).

LaTeX

$$$\uparrow (iInf i, S_i) = \bigcap_i \uparrow (S_i)$$$

Lean4

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

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