supClosed — Mathlib

English

A closure operator on sets is defined by generating all finite suprema of elements from the set, and taking the supremum closure of those collections.

Русский

Замыкание множества определяется как порождение конечных объединений и взятие их верхней границы.

LaTeX

$$supClosure : ClosureOperator(Set α)$$

Lean4

@[simp]
protected theorem supClosed (s : Set α) : SupClosed s := fun a ha b hb ↦ by cases le_total a b <;> simp [*]

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