α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
⊢ ↑(partialSups f) n ≤ ↑(partialSups g) n
α : Type u_1
inst✝ : SemilatticeSup α
⊢ Monotone partialSups
rintro f g h n
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
⊢ ↑(partialSups f) Nat.zero ≤ ↑(partialSups g) Nat.zero

case succ
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
ih : ↑(partialSups f) n ≤ ↑(partialSups g) n
⊢ ↑(partialSups f) (Nat.succ n) ≤ ↑(partialSups g) (Nat.succ n)
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
⊢ ↑(partialSups f) n ≤ ↑(partialSups g) n
induction' n with n ih
no goals
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
⊢ ↑(partialSups f) Nat.zero ≤ ↑(partialSups g) Nat.zero
exact h 0
no goals
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
ih : ↑(partialSups f) n ≤ ↑(partialSups g) n
⊢ ↑(partialSups f) (Nat.succ n) ≤ ↑(partialSups g) (Nat.succ n)
exact sup_le_sup ih (h _)