sups

Mathlib.Data.Set.Sups

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

English

If s.Nonempty and t.Nonempty, then (s ⊻ t).Nonempty.

Русский

Если s и t непустые, то (s ⊻ t) непусто.

LaTeX

$$$ s.Nonempty \rightarrow t.Nonempty \rightarrow (s \ ⊻ \ t).Nonempty$$$

Lean4

protected theorem sups : s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty :=
  Nonempty.image2

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

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

Разделы

Аффилиация

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