Nonempty — Mathlib

English

A Finset s is nonempty if and only if there exists an element x with x ∈ s.

Русский

Финитное множество s непусто тогда, когда существует элемент x, такой что x ∈ s.

LaTeX

$$s.Nonempty$$

Lean4

/-- The property `s.Nonempty` expresses the fact that the finset `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 : Finset α) : Prop :=
  ∃ x : α, x ∈ s

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