diff_iInter

Mathlib.Data.Set.Lattice

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

English

Let s be a set and t_i a family of sets. Then s \ ⋂_i t_i = ⋃_i (s \ t_i).

Русский

Пусть s — множество, t_i — семейство множеств. Тогда s \ ⋂_i t_i = ⋃_i (s \ t_i).

LaTeX

$$$ s \\bigcap_i t_i = \bigcup_i (s \\ t_i) $$$

Lean4

theorem diff_iInter (s : Set β) (t : ι → Set β) : (s \ ⋂ i, t i) = ⋃ i, s \ t i := by
  rw [diff_eq, compl_iInter, inter_iUnion]; rfl

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

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

Разделы

Аффилиация

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