Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix merge
Browse files Browse the repository at this point in the history
  • Loading branch information
collares committed May 26, 2023
1 parent bee9b84 commit 646cd3b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/algebra/infinite_sum/order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ variables [ordered_comm_monoid α] [topological_space α] [order_closed_topology

@[to_additive]
lemma has_prod_le (h : ∀ i, f i ≤ g i) (hf : has_prod f a₁) (hg : has_prod g a₂) : a₁ ≤ a₂ :=
le_of_tendsto_of_tendsto' hf hg $ λ s, finset.prod_le_prod'' $ λ b _, h b
le_of_tendsto_of_tendsto' hf hg $ λ s, finset.prod_le_prod' $ λ b _, h b

@[to_additive]
lemma has_prod_mono (hf : has_prod f a₁) (hg : has_prod g a₂) (h : f ≤ g) : a₁ ≤ a₂ :=
Expand Down

0 comments on commit 646cd3b

Please sign in to comment.