fst_image_sigma_subset

Mathlib.Data.Set.Sigma

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

English

The image of s.sigma t under fst is contained in s.

Русский

Образ сигмы fst над s.sigma t содержится в s.

LaTeX

$$$ \\Sigma^{\\mathrm{fst}} '' (s \\sigma t) \\subseteq s $$$

Lean4

theorem fst_image_sigma_subset (s : Set ι) (t : ∀ i, Set (α i)) : Sigma.fst '' s.sigma t ⊆ s :=
  image_subset_iff.2 fun _ ↦ And.left

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

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

Разделы

Аффилиация

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