coe_iInf — Mathlib

English

The underlying set of an iInf of a family is the intersection of the underlying sets: ↑(⨅ i, S_i) = ⋂ i, ↑(S_i).

Русский

Множество пересечения семейства подалгебр равно пересечению их множеств.

LaTeX

$$$↑(\\iInf_i S_i) = \\bigcap_i ↑S_i$$$

Lean4

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

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