Theorems · Theorem · general topology
Filter.tendsto_fst
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.fst (f ×ˢ g) f- Defined in
- Mathlib.Order.Filter.Prod
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.Tendstostatement · cited by 3,814
- SProd.sprodstatement · cited by 1,750
- Filter.tendsto_comapproof · cited by 30
- Filter.tendsto_inf_leftproof · cited by 10
Cited by26
Results whose statement or proof uses this declaration.
- Filter.prod_map_map_eqproof · cited by 17
- hasStrictFDerivAt_uncurry_coprodproof · cited by 5
- AffineSpace.asymptoticNhds_eq_smulproof · cited by 4
- intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_aeproof · cited by 2
- hasFDerivAt_of_tendstoUniformlyOnFilterproof · cited by 2
- CauchyFilter.inseparable_iff_of_le_nhdsproof · cited by 2
- Filter.Tendsto.tendstoUniformlyOnFilter_constproof · cited by 2
- Filter.prod_le_prodproof · cited by 2
- hasFDerivWithinAt_closure_of_tendsto_fderivproof · cited by 2
- HasFPowerSeriesWithinOnBall.tendsto_partialSum_prodproof · cited by 2
- Frullani.tendsto_intervalIntegralproof · cited by 1
- StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticConeproof · cited by 1