Nonempty — Mathlib

English

The property Nonempty(s) expresses that the set s is not empty, and by definition Nonempty(s) = ∃ x, x ∈ s.

Русский

Свойство Nonempty(s) выражает, что множество s не пусто; по определению Nonempty(s) = ∃ x, x ∈ s.

LaTeX

$$$\mathrm{Nonempty}(s) \iff \exists x\in s.$$$$

Lean4

/-- The property `s.Nonempty` expresses the fact that the set `s` is not empty. It should be used
in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
to the dot notation. -/
protected def Nonempty (s : Set α) : Prop :=
  ∃ x, x ∈ s

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