sigma_snd

Mathlib.Data.Set.Sigma

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.sigma_snd

English

If (s.sigma t).Nonempty, then there exists i ∈ s with (t i).Nonempty.

Русский

Если сигма-объединение непусто, то существует i ∈ s такое, что t i непусто.

LaTeX

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

Lean4

theorem sigma_snd : (s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty := fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1, x.2, hx.2⟩

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

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

Разделы

Аффилиация

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