inter_iUnion

Mathlib.Data.Set.Lattice

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

English

The intersection distributes over a union: s ∩ (⋃ i t_i) = ⋃ i (s ∩ t_i).

Русский

Пересечение распределяется по объединению: s ∩ (⋃ i t_i) = ⋃ i (s ∩ t_i).

LaTeX

$$$$ s \\cap \\bigcup_{i} t_i = \\bigcup_{i} (s \\cap t_i) $$$$

Lean4

theorem inter_iUnion (s : Set β) (t : ι → Set β) : (s ∩ ⋃ i, t i) = ⋃ i, s ∩ t i :=
  inf_iSup_eq _ _

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

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

Разделы

Аффилиация

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