sdiff_nonempty

Mathlib.Data.Finset.SDiff

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

English

The difference (s \ t) is nonempty iff s is not a subset of t.

Русский

Разность (s \ t) непустая тогда, когда s не является подмножеством t.

LaTeX

$$$ (s \setminus t).Nonempty \iff \neg (s \subseteq t) $$$

Lean4

@[grind =]
theorem sdiff_nonempty : (s \ t).Nonempty ↔ ¬s ⊆ t :=
  nonempty_iff_ne_empty.trans sdiff_eq_empty_iff_subset.not

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

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

Разделы

Аффилиация

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