iInter_vsub_subset

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

Let s i ⊆ β and t ⊆ β. Then (⋂ i s_i) -ᵥ t ⊆ ⋂ i (s_i -ᵥ t).

Русский

Пусть s_i ⊆ β; тогда (⋂_{i} s_i) -ᵥ t ⊆ ⋂_{i} (s_i -ᵥ t).

LaTeX

$$$\\left(\\bigcap_{i} s_i\\right) -_v t \\subseteq \\bigcap_{i} (s_i -_v t)$$$

Lean4

theorem iInter_vsub_subset (s : ι → Set β) (t : Set β) : (⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t :=
  image2_iInter_subset_left ..

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

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

Разделы

Аффилиация

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