image_sigmaMk_subset_sigma_right

Mathlib.Data.Set.Sigma

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

English

If i ∈ s, then the slice { (i, x) : x ∈ t(i) } is contained in s.sigma t.

Русский

Если i ∈ s, то множество { (i, x) : x ∈ t(i) } вложено в s.sigma t.

LaTeX

$$$\\text{if } i \\in s, \\; (\\{(i, x) : x \\in t(i)\\}) \\subseteq s \\sigma t$$$

Lean4

theorem image_sigmaMk_subset_sigma_right (hi : i ∈ s) : Sigma.mk i '' t i ⊆ s.sigma t :=
  image_subset_iff.2 fun _ ↦ And.intro hi

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

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

Разделы

Аффилиация

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