Basic properties of omega-complete partial orders

This file is a placeholder for lemmas about OmegaCompletePartialOrder. As the library grows, compatibility helpers specific to this project can be added here.

@[simp]

theorem OmegaCompletePartialOrder.ωSup_const {A : Type u_1} [OmegaCompletePartialOrder A] (x : A) : ωSup (Chain.const x) = x