Subsingleton — Mathlib

English

A set s is subsingleton if it has at most one element: every two elements of s are equal.

Русский

Множество s является субоднозначным, если в нём не более одного элемента: любые два элемента s равны.

LaTeX

$$$ \forall x \in s \; \forall y \in s,\; x = y $$$

Lean4

/-- A set `s` is a `Subsingleton` if it has at most one element. -/
protected def Subsingleton (s : Set α) : Prop :=
  ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), x = y

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