diff_iUnion

Mathlib.Data.Set.Lattice

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

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 \\bigcup_i t_i = \bigcap_i (s \\ t_i) $$$

Lean4

theorem diff_iUnion [Nonempty ι] (s : Set β) (t : ι → Set β) : (s \ ⋃ i, t i) = ⋂ i, s \ t i := by
  rw [diff_eq, compl_iUnion, inter_iInter]; rfl

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

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

Разделы

Аффилиация

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