Theorems · Theorem · general topology
UniformContinuous.prodMk
∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
{f₁ : α → β} {f₂ : α → γ}, UniformContinuous f₁ → UniformContinuous f₂ → UniformContinuous fun a => (f₁ a, f₂ a)- Defined in
- Mathlib.Topology.UniformSpace.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterproof · cited by 8,121
- Filter.Tendstoproof · cited by 3,814
- UniformSpacestatement and proof · cited by 2,040
- uniformityproof · cited by 765
- UniformContinuousstatement and proof · cited by 410
- Filter.tendsto_comap_iffproof · cited by 55
- Filter.tendsto_infproof · cited by 23
- uniformity_prodproof · cited by 2
Cited by18
Results whose statement or proof uses this declaration.
- UniformContinuous.prodMapproof · cited by 17
- UniformContinuous.subproof · cited by 4
- UniformContinuous.divproof · cited by 3
- UniformContinuous.prod_compactsproof · cited by 0
- UniformContinuous.prod_nonemptyCompactsproof · cited by 0
- UniformContinuous.sup_closedsproof · cited by 0
- UniformContinuous.sup_compactsproof · cited by 0
- UniformContinuous.sup_nonemptyCompactsproof · cited by 0
- IsUniformGroup.mk'proof · cited by 0
- uniformContinuous_swapproof · cited by 0
- UniformContinuous.distproof · cited by 0
- IsUniformAddGroup.mk'proof · cited by 0