insert_sigma

Mathlib.Data.Set.Sigma

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

English

Let s ⊆ ι, t: ∀ i, Set(α i), and a(i) ∈ α i. Then (insert i s).sigma t equals Sigma.mk i '' t i ∪ s.sigma t.

Русский

Пусть s ⊆ ι, t: ∀ i, Set(α i), и a(i) ∈ α i. Тогда (insert i s).sigma t равно Sigma.mk i '' t i ∪ s.sigma t.

LaTeX

$$$(\mathrm{insert}\ i\ s) \sigma t = \Sigma i, t i \;''\; t i \cup s \sigma t$$$

Lean4

theorem insert_sigma : (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t := by grind

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

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

Разделы

Аффилиация

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