partiallyWellOrderedOn_singleton — Mathlib

English

A singleton set {a} is partially well-ordered by any relation r that is reflexive on α.

Русский

Единственный элемент множества {a} частично хорошо упорядочен по любому отношению r, если r рефлексивно на α.

LaTeX

$$$PartiallyWellOrderedOn { a } r$$$

Lean4

@[simp]
theorem partiallyWellOrderedOn_singleton (a : α) : PartiallyWellOrderedOn { a } r :=
  (finite_singleton a).partiallyWellOrderedOn

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