le — Mathlib · SciLib

English

In a preorder, if the type is subsingleton, then any two elements satisfy x ≤ y.

Русский

В частном порядке, если множество является одиночным, то любые два элемента удовлетворяют неравенству x ≤ y.

LaTeX

$$$[\text{Preorder}(\alpha)] \land [\text{Subsingleton}(\alpha)] \Rightarrow \forall x,y:\, \alpha,\ x \le y$$$

Lean4

@[nontriviality]
protected theorem le [Preorder α] [Subsingleton α] (x y : α) : x ≤ y :=
  le_of_eq (Subsingleton.elim x y)

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