iInter₂_subset

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.iInter₂_subset

English

For s : ∀ i, κ i → Set α, and i,j, ∩ (i) (j), s i j ⊆ s i j.

Русский

Для заданного множества s(i)(j) имеем ∩_{i,j} s(i)(j) ⊆ s(i)(j) для любых i, j.

LaTeX

$$$\forall i, \forall j,\ \bigcap_{i'} \bigcap_{j'} s_{i' j'} \subseteq s_{i j}$$$

Lean4

theorem iInter₂_subset {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : ⋂ (i) (j), s i j ⊆ s i j :=
  iInf₂_le i j

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

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

Разделы

Аффилиация

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