sigma_subset_preimage_fst

Mathlib.Data.Set.Sigma

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

English

The sigma-set s.sigma t is contained in the preimage of s under the first projection.

Русский

Множество σ-суммы s.sigma t вложено в прообраз по первой проекции (fst) множества s.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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