sInter_pair

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.sInter_pair

English

Let s and t be subsets of α. The intersection over the two-element set {s, t} equals s ∩ t: ⋂₀ { s, t } = s ∩ t.

Русский

Пусть s и t — подмножества α. Пересечение над двумя элементами {s, t} равно s ∩ t: ⋂₀ { s, t } = s ∩ t.

LaTeX

$$$$ \\bigcap_{U \\in \\{s, t\\}} U = s \\cap t. $$$$

Lean4

theorem sInter_pair (s t : Set α) : ⋂₀ { s, t } = s ∩ t :=
  sInf_pair

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

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

Разделы

Аффилиация

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