Theorems · Theorem · order theory

ScottContinuousOn.monotone

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} (D : Set (Set α)),
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) → ScottContinuousOn D f → Monotone f

Defined in

Mathlib.Order.ScottContinuity

Cited by

5 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder