Commit 2022-02-15 15:52 9307f5b4
View on Github →feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003)
Prove this lemma and its inf
counterpart:
lemma filter.tendsto.sup_right_nhds {ι β} [topological_space β] [has_sup β] [has_continuous_sup β]
{l : filter ι} {f g : ι → β} {x y : β} (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) :
tendsto (f ⊔ g) l (𝓝 (x ⊔ y))
The name is sup_right_nhds
because sup
already exists, and is about a supremum over the filters on the left in the tendsto.
The proofs of tendsto_prod_iff'
and prod.tendsto_iff
were written by Patrick Massot.