vsub_sInter_subset

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

Let s ⊆ β and T ⊆ Set β. Then s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t.

Русский

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

LaTeX

$$$s -_v \\bigcap_{0} T \\subseteq \\bigcap_{t \\in T} (s -_v t)$$$

Lean4

theorem vsub_sInter_subset (s : Set β) (T : Set (Set β)) : s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t :=
  image2_sInter_subset_right ..

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

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

Разделы

Аффилиация

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