biInter_pair

Mathlib.Data.Set.Lattice

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

English

For any a,b, the intersection over x ∈ {a,b} of s(x) equals s(a) ∩ s(b).

Русский

Для любых a,b пересечение по x ∈ {a,b} множества s(x) равно s(a) ∩ s(b).

LaTeX

$$$\\\\bigcap_{x \\in \\{ a, b \\}} s(x) = s(a) \\cap s(b)$$$

Lean4

theorem biInter_pair (a b : α) (s : α → Set β) : ⋂ x ∈ ({ a, b } : Set α), s x = s a ∩ s b := by
  rw [biInter_insert, biInter_singleton]

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

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

Разделы

Аффилиация

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