iInter_mono''

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.iInter_mono''

English

If s_i ⊆ t_i for all i, then iInter s ⊆ iInter t.

Русский

Если s_i ⊆ t_i для всех i, то iInter s ⊆ iInter t.

LaTeX

$$$\forall i,\ s_i \subseteq t_i \Rightarrow \bigcap_i s_i \subseteq \bigcap_i t_i$$$

Lean4

@[gcongr]
theorem iInter_mono'' {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iInter s ⊆ iInter t :=
  iInf_mono h

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

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

Разделы

Аффилиация

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