α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ (⨆ (n : ℕ), ↑(partialSups f) n) ≤ ⨆ (n : ℕ), ↑(partialSups g) n
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ (⨆ (n : ℕ), f n) ≤ ⨆ (n : ℕ), g n
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
no goals
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ (⨆ (n : ℕ), ↑(partialSups f) n) ≤ ⨆ (n : ℕ), ↑(partialSups g) n
exact iSup_mono h