Theorems · Theorem · order theory

ScottContinuousOn.fromProd

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α × β → γ} {D : Set (Set (α × β))},
  (∀ (a : α), ScottContinuousOn ((fun d => Prod.snd '' d) '' D) fun b => f (a, b)) →
    (∀ (b : β), ScottContinuousOn ((fun d => Prod.fst '' d) '' D) fun a => f (a, b)) →
      (∀ (a : α), Monotone fun b => f (a, b)) → (∀ (b : β), Monotone fun a => f (a, b)) → ScottContinuousOn D f

If is Scott continuous on a product space if it is Scott continuous and monotone in each variable

Defined in

Mathlib.Order.ScottContinuity.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderPreorderPreorder