sInter_vsub_subset

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

Let S be a set of subsets of β and t ⊆ β. Then ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t.

Русский

Пусть S — множество подмножеств β. Тогда ⋂₀ S -ᵥ t ⊆ ⋂_{s∈S} (s -ᵥ t).

LaTeX

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

Lean4

theorem sInter_vsub_subset (S : Set (Set β)) (t : Set β) : ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t :=
  image2_sInter_subset_left ..

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

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

Разделы

Аффилиация

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