union_nonempty

Mathlib.Data.Finset.Lattice.Lemmas

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

English

The nonemptiness of the union s ∪ t is equivalent to s Nonempty or t Nonempty.

Русский

Непустость объединения эквивалентна тому, что хотя бы одно из множеств непустое.

LaTeX

$$s.Nonempty ∨ t.Nonempty ↔ (s ∪ t).Nonempty$$

Lean4

@[simp]
theorem union_nonempty : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty :=
  mod_cast Set.union_nonempty (α := α) (s := s) (t := t)

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

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

Разделы

Аффилиация

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