Minimal elements of upper closures

[UPSTREAM] candidate for Mathlib/Order/UpperLower/Closure.lean: in a partial order, the minimal elements of an upper closure are those of the generating set, and so is its least element. mathlib has the minimal-element lemma only for antichains, IsAntichain.minimal_mem_upperClosure_iff_mem, which follows from the general one with IsAntichain.minimal_mem_iff.

theorem minimal_mem_upperClosure_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} : Minimal (fun (x : α) => x ∈ upperClosure s) x ↔ Minimal (fun (x : α) => x ∈ s) x

The minimal elements of the upper closure of s are those of s.

theorem maximal_mem_lowerClosure_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} : Maximal (fun (x : α) => x ∈ lowerClosure s) x ↔ Maximal (fun (x : α) => x ∈ s) x

The maximal elements of the lower closure of s are those of s.

theorem isLeast_upperClosure_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} : IsLeast (↑(upperClosure s)) x ↔ IsLeast s x

A set and its upper closure have the same least element.

theorem isGreatest_lowerClosure_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} : IsGreatest (↑(lowerClosure s)) x ↔ IsGreatest s x

A set and its lower closure have the same greatest element.