mk_mem_sigma

Mathlib.Data.Set.Sigma

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

English

If i ∈ s and a ∈ t i, then ⟨i,a⟩ ∈ s.sigma t.

Русский

Если i ∈ s и a ∈ t i, то ⟨i,a⟩ ∈ s.sigma t.

LaTeX

$$$(hi:\\ i \\in s) (ha:\\ a \\in t i) \\Rightarrow (\\langle i,a\\rangle : \\Sigma i, \\alpha i) \\in s.\\sigma t$$$

Lean4

theorem mk_mem_sigma (hi : i ∈ s) (ha : a ∈ t i) : (⟨i, a⟩ : Σ i, α i) ∈ s.sigma t :=
  ⟨hi, ha⟩

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

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

Разделы

Аффилиация

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