sigma_nonempty_iff

Mathlib.Data.Set.Sigma

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

English

Equivalence: (s.sigma t).Nonempty iff ∃ i ∈ s, (t i).Nonempty.

Русский

Эквивалентность: (s.sigma t).Nonempty эквивалентно ∃ i ∈ s, (t i).Nonempty.

LaTeX

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

Lean4

theorem sigma_nonempty_iff : (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty :=
  ⟨Nonempty.sigma_snd, fun ⟨i, hi, a, ha⟩ ↦ ⟨⟨i, a⟩, hi, ha⟩⟩

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

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

Разделы

Аффилиация

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