α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
⊢ Monotone f
intro a b hab
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ f '' {a, b}
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ≤ f b
apply e1.1
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ {f a, f b}
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ f '' {a, b}
rw [Set.image_pair]
no goals
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ {f a, f b}
exact Set.mem_insert _ _
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ Set.Nonempty {a, b}

case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ DirectedOn (fun x x_1 => x ≤ x_1) {a, b}

case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB (f '' {a, b}) (f b)
apply h
no goals
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ Set.Nonempty {a, b}
exact Set.insert_nonempty _ _
no goals
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ DirectedOn (fun x x_1 => x ≤ x_1) {a, b}
exact directedOn_pair le_refl hab
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLeast (Set.Ici b) b
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b
rw [IsLUB, upperBounds_insert, upperBounds_singleton,
  Set.inter_eq_self_of_subset_right (Set.Ici_subset_Ici.mpr hab)]
no goals
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLeast (Set.Ici b) b
exact isLeast_Ici