coe_sInf

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.coe_sInf

English

The carrier of sInf S equals the intersection over S of their carriers.

Русский

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

LaTeX

$$$$ ((sInf S : L.Substructure M) : Set M) = \bigcap_{S \in S} (S : Set M) $$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (L.Substructure M)) : ((sInf S : L.Substructure M) : Set M) = ⋂ s ∈ S, (s : Set M) :=
  rfl

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

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

Разделы

Аффилиация

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