def OmegaCompletePartialOrder.Chain.const {A : Type u_1} [Preorder A] (x : A) : Chain A

The chain that always returns the same value.

Equations

• OmegaCompletePartialOrder.Chain.const x = (OrderHom.const ℕ) x

@[simp]

theorem OmegaCompletePartialOrder.Chain.const_apply {A : Type u_1} [Preorder A] (x : A) (n : ℕ) : (const x) n = x