biInter_subset_biInter_left

Mathlib.Data.Set.Lattice

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

← MathLib Explorer

English

If s' ⊆ s, then ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x.

Русский

Если s' ⊆ s, тогда ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x.

LaTeX

$$$$ s' \\subseteq s \\Rightarrow \\bigcap_{x \\in s} t(x) \\subseteq \\bigcap_{x \\,\\in\\, s'} t(x). $$$$

Lean4

theorem biInter_subset_biInter_left {s s' : Set α} {t : α → Set β} (h : s' ⊆ s) : ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x :=
  subset_iInter₂ fun _ hx => biInter_subset_of_mem <| h hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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