nonempty_iff_ne_empty'

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.nonempty_iff_ne_empty'

English

Nonempty s iff Ne empty s (variant).

Русский

Непустотa s эквивалентна Ne пустому (вариант).

LaTeX

$$$$ \operatorname{Nonempty}(s) \iff \operatorname{Ne}(s, \emptyset). $$$$

Lean4

/-- See also `not_nonempty_iff_eq_empty'`. -/
theorem nonempty_iff_ne_empty' : Nonempty s ↔ s ≠ ∅ :=
  not_nonempty_iff_eq_empty'.not_right

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

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

Разделы

Аффилиация

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