sigma_fst

Mathlib.Data.Set.Sigma

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

English

If (s.sigma t) is nonempty, then s is nonempty.

Русский

Если сигма-объединение по s непусто, то s непусто.

LaTeX

$$$(s.\sigma t).\text{Nonempty} \Rightarrow s.\text{Nonempty}$$$

Lean4

theorem sigma_fst : (s.sigma t).Nonempty → s.Nonempty := fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1⟩

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

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

Разделы

Аффилиация

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