Nontrivial — Mathlib

English

A set is nontrivial if it contains at least two distinct elements.

Русский

Множество не тривиально, если в нем содержатся хотя бы два различных элемента.

LaTeX

$$$ \text{Set.Nontrivial}(s) :\equiv\ ∃ x ∈ s, ∃ y ∈ s, x ≠ y $$$

Lean4

/-- A set `s` is `Set.Nontrivial` if it has at least two distinct elements. -/
protected def Nontrivial (s : Set α) : Prop :=
  ∃ x ∈ s, ∃ y ∈ s, x ≠ y

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