subset_iUnion₂

Mathlib.Data.Set.Lattice

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

English

Given s(i)(j) as a family of sets, s(i)(j) ⊆ ⋃(i')(j'), s(i')(j').

Русский

Для каждой пары индексов i, j множество s(i)(j) вложено в объединение ⋃(i')(j') s(i')(j').

LaTeX

$$$s_{ij} \subseteq \bigcup_{i',j'} s_{i' j'}$$$

Lean4

theorem subset_iUnion₂ {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : s i j ⊆ ⋃ (i') (j'), s i' j' :=
  le_iSup₂ i j

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

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

Разделы

Аффилиация

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