upperClosure_eq — Mathlib

English

A set equals its upper closure exactly when it is an upper set.

Русский

Множество равно своему верхнему замыканию тогда, когда оно является верхним множеством.

LaTeX

$$$ \\uparrow(\\operatorname{upperClosure}(s)) = s \\iff \\operatorname{IsUpperSet}(s) $$$

Lean4

@[simp]
theorem upperClosure_eq : ↑(upperClosure s) = s ↔ IsUpperSet s :=
  ⟨(· ▸ UpperSet.upper _), IsUpperSet.upperClosure⟩

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