upperClosure_singleton — Mathlib

English

The upper closure of a singleton {a} is the principal up-set {x : a ≤ x}.

Русский

Верхнее замыкание множества, состоящего из одного элемента a, равно множеству элементов больше или равных a.

LaTeX

$$$\mathrm{upperClosure}(({a}) ) = \mathrm{UpperSet.Ici a}$$$

Lean4

@[simp]
theorem upperClosure_singleton (a : α) : upperClosure ({ a } : Set α) = UpperSet.Ici a :=
  by
  ext
  simp

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