vsub_iInter_subset

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

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

Русский

Пусть s ⊆ β и t_i ⊆ Set β. Тогда s -ᵥ ⋂_{i} t_i ⊆ ⋂_{i} (s -ᵥ t_i).

LaTeX

$$$s -_v \\bigcap_{i} t_i \\subseteq \\bigcap_{i} (s -_v t_i)$$$

Lean4

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

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

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

Разделы

Аффилиация

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