coe_sInf

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

Underlying set of sInf t equals the intersection over t.

Русский

Основанное множество sInf t равно пересечению по t.

LaTeX

$$$(sInf t : AffineSubspace k P) : Set P = \bigcap_{s \in t} (s : Set P)$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (t : Set (AffineSubspace k P)) : ((sInf t : AffineSubspace k P) : Set P) = ⋂ s ∈ t, s :=
  rfl

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

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

Разделы

Аффилиация

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