LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Const

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Const.

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 = { toOrderHom := (OrderHom.const ℕ) x }

@[simp]

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