no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
⊢ LeftOrdContinuous (f^[n])
induction n with
| zero => exact LeftOrdContinuous.id α
| succ n ihn => exact ihn.comp hf
no goals
case zero
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
⊢ LeftOrdContinuous (f^[Nat.zero])
exact LeftOrdContinuous.id α
no goals
case succ
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f✝ : α → β
f : α → α
hf : LeftOrdContinuous f
n : ℕ
ihn : LeftOrdContinuous (f^[n])
⊢ LeftOrdContinuous (f^[Nat.succ n])
exact ihn.comp hf