mem_sigma

Mathlib.Data.Finset.Sigma

URI: https://scilib.ai/kg/mathlib#Finset.mem_sigma

English

A simplification variant of sigma_nonempty.

Русский

Упрощённый вариант sigma_nonempty.

LaTeX

$$$ (s.sigma t).Nonempty \iff \exists i \in s, (t i).Nonempty $$$

Lean4

@[simp]
theorem mem_sigma {a : Σ i, α i} : a ∈ s.sigma t ↔ a.1 ∈ s ∧ a.2 ∈ t a.1 :=
  Multiset.mem_sigma

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

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

Разделы

Аффилиация

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