coe_sInf

Mathlib.Order.BooleanSubalgebra

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

English

The carrier of the infimum of a set S of Boolean subalgebras equals the intersection over S of their carriers.

Русский

Носитель пересечения InfSet S равен пересечению носителей всех элементов S.

LaTeX

$$sInf S = ⋂ L ∈ S, (L : Set α)$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (BooleanSubalgebra α)) : sInf S = ⋂ L ∈ S, (L : Set α) :=
  rfl

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

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

Разделы

Аффилиация

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