coe_iInf

Mathlib.Order.BooleanSubalgebra

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

English

The iInf (indexed infimum) of a family f i of Boolean subalgebras equals the intersection of their carriers.

Русский

Совокупный по индексу Inf i f(i) равен пересечению носителей всех f(i).

LaTeX

$$⨅ i, f i = ⋂ i, (f i : Set α)$$

Lean4

@[simp, norm_cast]
theorem coe_iInf (f : ι → BooleanSubalgebra α) : ⨅ i, f i = ⋂ i, (f i : Set α) := by simp [iInf]

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

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

Разделы

Аффилиация

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