Theorems · Definition · general topology
UniformFun.gen
(α : Type u_1) → (β : Type u_2) → Set (β × β) → Set (UniformFun α β × UniformFun α β)
Basis sets for the uniformity of uniform convergence: gen α β V is the set of pairs (f, g)
of functions α →ᵤ β such that ∀ x, (f x, g x) ∈ V.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses 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.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Set.ofPredproof · cited by 6,101
- UniformFunstatement and proof · cited by 106
- UniformFun.toFunproof · cited by 47
Cited by17
Results whose statement or proof uses this declaration.
- UniformFun.hasBasis_uniformitystatement · cited by 12
- UniformFun.hasBasis_uniformity_of_basisstatement and proof · cited by 8
- UniformFun.hasBasis_nhds_of_basisstatement · cited by 7
- UniformFun.hasBasis_nhdsstatement · cited by 5
- UniformFun.tendsto_iff_tendstoUniformlyproof · cited by 4
- Equicontinuous.comap_uniformFun_eqproof · cited by 3
- UniformFun.precomp_uniformContinuousproof · cited by 2
- UniformOnFun.uniformity_eq_of_basisproof · cited by 2
- UniformFun.uniformContinuous_evalproof · cited by 2
- UniformFun.hasBasis_nhds_zero_of_basisproof · cited by 1
- UniformFun.uniformSpace_eq_iInf_precomp_of_coverproof · cited by 1
- UniformFun.uniformSpace_eq_inf_precomp_of_coverproof · cited by 1