Principal closure operators

[UPSTREAM] candidate for Mathlib/Order/Closure.lean.

On a join-semilattice, joining with a fixed element a is a closure operator whose closed elements are those above a. On a join-semilattice with a bottom element, these principal closure operators are exactly the closure operators whose closed elements form an upper set: such an operator joins its argument with the closure of ⊥.

Main definitions

• ClosureOperator.supRight: the closure operator (· ⊔ a).

Main results

• ClosureOperator.isClosed_supRight_iff: the closed elements of (· ⊔ a) are those above a.
• ClosureOperator.eq_supRight_iff: a closure operator is (· ⊔ c ⊥) exactly when its closed elements form an upper set.

def ClosureOperator.supRight {α : Type u_1} [SemilatticeSup α] (a : α) : ClosureOperator α

The principal closure operator (· ⊔ a), whose closed elements are those above a.

Equations

• ClosureOperator.supRight a = ClosureOperator.mk' (fun (x : α) => x ⊔ a) ⋯ ⋯ ⋯

@[simp]

theorem ClosureOperator.supRight_apply {α : Type u_1} [SemilatticeSup α] (a x✝ : α) : (supRight a) x✝ = x✝ ⊔ a

theorem ClosureOperator.isClosed_supRight_iff {α : Type u_1} [SemilatticeSup α] {a x : α} : (supRight a).IsClosed x ↔ a ≤ x

theorem ClosureOperator.isUpperSet_setOf_isClosed_supRight {α : Type u_1} [SemilatticeSup α] (a : α) : IsUpperSet {x : α | (supRight a).IsClosed x}

theorem ClosureOperator.eq_supRight_iff {α : Type u_1} [SemilatticeSup α] [OrderBot α] (c : ClosureOperator α) : c = supRight (c ⊥) ↔ IsUpperSet {x : α | c.IsClosed x}

A closure operator joins its argument with the closure of ⊥ exactly when its closed elements form an upper set.