Theorems · Definition · order theory

OmegaCompletePartialOrder.ContinuousHom.ofFun

{α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] →
        (f : α → β) →
          autoParam (OmegaCompletePartialOrder.ωScottContinuous f)
              OmegaCompletePartialOrder.ContinuousHom.ofFun._auto_1 →
            α →𝒄 β

Constructs a ContinuousHom from a function f and a proof of ωScottContinuous f. By default, the proof is inferred by fun_prop, which makes it ideal for simple cases.

Defined in

Mathlib.Order.OmegaCompletePartialOrder

Cited by

1 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

OmegaCompletePartialOrderOmegaCompletePartialOrder