UniformConvergenceTopology

📁 Source: Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Statistics

Metric	Count
Definitions «term_→ᵤ[_]_», «term_→ᵤ_», UniformFun, basis, congrLeft, congrRight, filter, gen, ofFun, phi, toFun, topologicalSpace, uniformCore, uniformEquivPiComm, uniformEquivProdArrow, uniformSpace, UniformOnFun, congrLeft, congrRight, gen, ofFun, toFun, topologicalSpace, uniformEquivPiComm, uniformEquivProdArrow, uniformEquivUniformFun, uniformSpace	27
Theorems comp_tendstoUniformly, comp_tendstoUniformlyOn_eventually, comp_tendstoUniformly_eventually, comap_eq, gc, hasBasis_nhds, hasBasis_nhds_of_basis, hasBasis_uniformity, hasBasis_uniformity_of_basis, iInf_eq, inf_eq, instCompleteSpace, instT2Space, isBasis_gen, isClosed_setOf_continuous, mem_gen, mono, ofFun_toFun, postcomp_isUniformEmbedding, postcomp_isUniformInducing, postcomp_uniformContinuous, precomp_uniformContinuous, tendsto_iff_tendstoUniformly, toFun_ofFun, uniformContinuous_eval, uniformContinuous_toFun, uniformSpace_eq_iInf_precomp_of_cover, uniformSpace_eq_inf_precomp_of_cover, comap_eq, continuousAt_eval₂, continuousOn_eval₂, continuous_rng_iff, gen_eq_preimage_restrict, gen_mem_nhds, gen_mem_uniformity, gen_mono, hasAntitoneBasis_uniformity, hasBasis_nhds, hasBasis_nhds_of_basis, hasBasis_uniformity, hasBasis_uniformity_of_basis, hasBasis_uniformity_of_basis_aux₁, hasBasis_uniformity_of_basis_aux₂, hasBasis_uniformity_of_covering_of_basis, iInf_eq, inf_eq, instCompleteSpace, isBasis_gen, isClosed_setOf_continuous, isCountablyGenerated_uniformity, isEmbedding_toFun_finite, isUniformEmbedding_toFun_finite, isUniformInducing_pi_restrict, mono, nhds_eq, nhds_eq_of_basis, ofFun_toFun, postcomp_isUniformEmbedding, postcomp_isUniformInducing, postcomp_uniformContinuous, precomp_uniformContinuous, t2Space_of_covering, tendsto_iff_tendstoUniformlyOn, toFun_ofFun, topologicalSpace_eq, uniformContinuous_eval, uniformContinuous_eval_of_mem, uniformContinuous_eval_of_mem_sUnion, uniformContinuous_ofFun_toFun, uniformContinuous_ofUniformFun, uniformContinuous_restrict, uniformContinuous_restrict_toFun, uniformContinuous_toFun, uniformSpace_eq_iInf_precomp_of_cover, uniformSpace_eq_inf_precomp_of_cover, uniformity_eq, uniformity_eq_of_basis, instNonemptyUniformFun, instNonemptyUniformOnFun, instSubsingletonUniformFun, instSubsingletonUniformOnFun	81
Total	108

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_tendstoUniformly 📖	—	Set Set.instMembership UniformContinuousOn TendstoUniformly	—	—	CanLift.prf Pi.canLift Subtype.canLift Filter.Tendsto.of_tendsto_comp tendstoUniformly_iff_tendsto Eq.le IsUniformInducing.comap_uniformity IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_subtype_val UniformContinuous.comp_tendstoUniformly uniformContinuousOn_iff_restrict
comp_tendstoUniformlyOn_eventually 📖	—	Filter.Eventually Set Set.instMembership UniformContinuousOn TendstoUniformlyOn	—	—	tendstoUniformlyOn_iff_restrict comp_tendstoUniformly_eventually
comp_tendstoUniformly_eventually 📖	—	Filter.Eventually Set Set.instMembership UniformContinuousOn TendstoUniformly	—	—	Filter.eventually_iff_exists_mem Filter.eventuallyEq_iff_exists_mem tendstoUniformly_congr comp_tendstoUniformly

UniformConvergence

Definitions

Name	Category	Theorems
«term_→ᵤ[_]_» 📖	CompOp	—
«term_→ᵤ_» 📖	CompOp	—

UniformFun

Definitions

Name	Category	Theorems
basis 📖	CompOp	—
congrLeft 📖	CompOp	—
congrRight 📖	CompOp	—
filter 📖	CompOp	1 math math: gc
gen 📖	CompOp	7 math math: UniformOnFun.gen_eq_preimage_restrict, hasBasis_uniformity, hasBasis_uniformity_of_basis, mem_gen, isBasis_gen, hasBasis_nhds_of_basis, hasBasis_nhds
ofFun 📖	CompOp	44 math math: Equicontinuous.inducing_uniformFun_iff_pi, ofFun_one, UniformOnFun.isometry_restrict, uniformSpace_eq_iInf_precomp_of_cover, toFun_ofFun, BoundedContinuousFunction.isEmbedding_coeFn, Equicontinuous.tendsto_uniformFun_iff_pi, equicontinuousWithinAt_iff_continuousWithinAt, postcomp_isUniformInducing, isometry_ofFun_continuousMap, equicontinuousOn_iff_continuousOn, UniformOnFun.continuous_rng_iff, isometry_ofFun_boundedContinuousFunction, ofFun_zero, ofFun_div, UniformOnFun.topologicalSpace_eq, lipschitzWith_ofFun_iff, equicontinuous_iff_continuous, ContinuousMap.continuous_iff_continuous_uniformFun, ofFun_smul, precomp_uniformContinuous, Equicontinuous.isUniformInducing_uniformFun_iff_pi, ofFun_prod, postcomp_uniformContinuous, ofFun_neg, UniformOnFun.uniformContinuous_restrict, UniformOnFun.edist_eq_pi_restrict, uniformEquicontinuousOn_iff_uniformContinuousOn, ContinuousMap.isUniformEmbedding_uniformFunOfFun, lipschitzOnWith_ofFun_iff, ofFun_sub, equicontinuousAt_iff_continuousAt, UniformOnFun.edist_eq_restrict_sUnion, ofFun_sum, ofFun_add, ofFun_toFun, UniformOnFun.isUniformInducing_pi_restrict, uniformSpace_eq_inf_precomp_of_cover, postcomp_isUniformEmbedding, UniformOnFun.lipschitzWith_restrict, ofFun_mul, uniformEquicontinuous_iff_uniformContinuous, BoundedContinuousFunction.isInducing_coeFn, ofFun_inv
phi 📖	CompOp	1 math math: gc
toFun 📖	CompOp	35 math math: UniformOnFun.gen_eq_preimage_restrict, edist_eval_le, UniformOnFun.uniformContinuous_ofUniformFun, uniformSpace_eq_iInf_precomp_of_cover, toFun_sub, UniformOnFun.lipschitzWith_one_ofFun_toFun, toFun_ofFun, postcomp_isUniformInducing, toFun_zero, tendsto_iff_tendstoUniformly, toFun_smul, edist_le, toFun_one, toFun_prod, toFun_div, dist_le, precomp_uniformContinuous, postcomp_uniformContinuous, edist_def, lipschitzWith_iff, mem_gen, toFun_neg, toFun_add, uniformContinuous_eval, uniformContinuous_toFun, toFun_inv, toFun_sum, ofFun_toFun, uniformSpace_eq_inf_precomp_of_cover, dist_def, toFun_mul, postcomp_isUniformEmbedding, lipschitzOnWith_iff, isClosed_setOf_continuous, lipschitzWith_eval
topologicalSpace 📖	CompOp	20 math math: Equicontinuous.inducing_uniformFun_iff_pi, BoundedContinuousFunction.isEmbedding_coeFn, hasBasis_nhds_zero_of_basis, Equicontinuous.tendsto_uniformFun_iff_pi, equicontinuousWithinAt_iff_continuousWithinAt, hasBasis_nhds_zero, instT2Space, tendsto_iff_tendstoUniformly, equicontinuousOn_iff_continuousOn, UniformOnFun.continuous_rng_iff, UniformOnFun.topologicalSpace_eq, hasBasis_nhds_one_of_basis, equicontinuous_iff_continuous, ContinuousMap.continuous_iff_continuous_uniformFun, hasBasis_nhds_one, equicontinuousAt_iff_continuousAt, hasBasis_nhds_of_basis, hasBasis_nhds, isClosed_setOf_continuous, BoundedContinuousFunction.isInducing_coeFn
uniformCore 📖	CompOp	—
uniformEquivPiComm 📖	CompOp	—
uniformEquivProdArrow 📖	CompOp	—
uniformSpace 📖	CompOp	28 math math: UniformOnFun.uniformContinuous_ofUniformFun, uniformSpace_eq_iInf_precomp_of_cover, instIsUniformAddGroupUniformFun, mono, hasBasis_uniformity, postcomp_isUniformInducing, instCompleteSpace, Equicontinuous.comap_uniformFun_eq, hasBasis_uniformity_of_basis, precomp_uniformContinuous, Equicontinuous.isUniformInducing_uniformFun_iff_pi, postcomp_uniformContinuous, UniformOnFun.uniformContinuous_restrict, uniformEquicontinuousOn_iff_uniformContinuousOn, ContinuousMap.isUniformEmbedding_uniformFunOfFun, instIsUniformGroupUniformFun, uniformContinuous_eval, uniformContinuous_toFun, uniformContinuousConstSMul, comap_eq, iInf_eq, UniformOnFun.isUniformInducing_pi_restrict, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, uniformSpace_eq_inf_precomp_of_cover, postcomp_isUniformEmbedding, UniformOnFun.hasBasis_uniformity_of_basis_aux₂, inf_eq, uniformEquicontinuous_iff_uniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_eq 📖	mathematical	—	uniformSpace UniformSpace.comap	—	IsUniformInducing.comap_uniformSpace postcomp_isUniformInducing
gc 📖	mathematical	—	GaloisConnection Filter UniformFun PartialOrder.toPreorder Filter.instPartialOrder Filter.map phi SProd.sprod Filter.instSProd Top.top Filter.instTop filter	—	filter.eq_1 FilterBasis.generate Filter.le_generate_iff Set.image_subset_iff Filter.mem_prod_top
hasBasis_nhds 📖	mathematical	—	Filter.HasBasis UniformFun Set nhds topologicalSpace Filter Filter.instMembership uniformity setOf Set.instMembership gen	—	hasBasis_nhds_of_basis Filter.basis_sets
hasBasis_nhds_of_basis 📖	mathematical	Filter.HasBasis uniformity	UniformFun nhds topologicalSpace setOf Set Set.instMembership gen	—	nhds_basis_uniformity' hasBasis_uniformity_of_basis
hasBasis_uniformity 📖	mathematical	—	Filter.HasBasis UniformFun Set uniformity uniformSpace Filter Filter.instMembership gen	—	Filter.IsBasis.hasBasis isBasis_gen
hasBasis_uniformity_of_basis 📖	mathematical	Filter.HasBasis uniformity	UniformFun uniformSpace Set gen	—	Filter.HasBasis.to_hasBasis hasBasis_uniformity Filter.HasBasis.mem_iff Filter.HasBasis.mem_of_mem subset_rfl Set.instReflSubset
iInf_eq 📖	mathematical	—	uniformSpace iInf UniformSpace instInfSetUniformSpace UniformFun	—	UniformSpace.ext iInf_uniformity GaloisConnection.u_iInf gc
inf_eq 📖	mathematical	—	uniformSpace UniformSpace instMinUniformSpace UniformFun	—	inf_eq_iInf iInf_eq iInf_congr
instCompleteSpace 📖	mathematical	—	CompleteSpace UniformFun uniformSpace	—	UniformEquiv.completeSpace_iff Set.mem_singleton UniformOnFun.instCompleteSpace
instT2Space 📖	mathematical	—	T2Space UniformFun topologicalSpace	—	T2Space.of_injective_continuous Pi.t2Space Equiv.injective UniformContinuous.continuous uniformContinuous_toFun
isBasis_gen 📖	mathematical	—	Filter.IsBasis UniformFun Set Filter Filter.instMembership gen	—	Filter.univ_mem Filter.inter_mem
isClosed_setOf_continuous 📖	mathematical	—	IsClosed UniformFun topologicalSpace setOf Continuous UniformSpace.toTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	isClosed_iff_forall_filter TendstoUniformly.continuous tendsto_iff_tendstoUniformly Filter.tendsto_id' Filter.Eventually.frequently Filter.le_principal_iff
mem_gen 📖	mathematical	—	UniformFun Set Set.instMembership gen DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	—
mono 📖	mathematical	—	Monotone UniformSpace UniformFun PartialOrder.toPreorder instPartialOrderUniformSpace uniformSpace	—	GaloisConnection.monotone_u gc
ofFun_toFun 📖	mathematical	—	DFunLike.coe Equiv UniformFun EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	—
postcomp_isUniformEmbedding 📖	mathematical	IsUniformEmbedding	UniformFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	postcomp_isUniformInducing IsUniformEmbedding.isUniformInducing IsUniformEmbedding.injective
postcomp_isUniformInducing 📖	mathematical	IsUniformInducing	UniformFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	Filter.HasBasis.eq_of_same_basis Filter.HasBasis.comap hasBasis_uniformity hasBasis_uniformity_of_basis IsUniformInducing.basis_uniformity Filter.basis_sets
postcomp_uniformContinuous 📖	mathematical	UniformContinuous	UniformFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	uniformContinuous_iff mono comap_eq
precomp_uniformContinuous 📖	mathematical	—	UniformContinuous UniformFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	UniformContinuous.eq_1 Filter.HasBasis.tendsto_iff hasBasis_uniformity
tendsto_iff_tendstoUniformly 📖	mathematical	—	Filter.Tendsto UniformFun nhds topologicalSpace TendstoUniformly DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	Filter.HasBasis.tendsto_right_iff hasBasis_nhds TendstoUniformly.eq_1
toFun_ofFun 📖	mathematical	—	DFunLike.coe Equiv UniformFun EquivLike.toFunLike Equiv.instEquivLike toFun ofFun	—	—
uniformContinuous_eval 📖	mathematical	—	UniformContinuous UniformFun uniformSpace Function.eval DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	Filter.map_le_iff_le_comap Filter.HasBasis.le_basis_iff hasBasis_uniformity Filter.HasBasis.comap Filter.basis_sets
uniformContinuous_toFun 📖	mathematical	—	UniformContinuous UniformFun uniformSpace Pi.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	uniformContinuous_pi uniformContinuous_eval
uniformSpace_eq_iInf_precomp_of_cover 📖	mathematical	Set.Finite Set.iUnion Set Set.instMembership Set.range Set.univ	uniformSpace iInf UniformSpace UniformFun instInfSetUniformSpace UniformSpace.comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	UniformSpace.ext iInf_uniformity le_antisymm le_iInf Filter.tendsto_iff_comap precomp_uniformContinuous Filter.HasBasis.le_basis_iff Filter.HasBasis.iInf Filter.HasBasis.comap hasBasis_uniformity Set.mem_iUnion₂ Eq.ge Set.mem_univ Set.mem_iInter
uniformSpace_eq_inf_precomp_of_cover 📖	mathematical	Set Set.instUnion Set.range Set.univ	uniformSpace UniformSpace UniformFun instMinUniformSpace UniformSpace.comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	UniformSpace.ext le_antisymm le_inf Filter.tendsto_iff_comap precomp_uniformContinuous Filter.HasBasis.le_basis_iff Filter.HasBasis.inf Filter.HasBasis.comap hasBasis_uniformity Eq.ge Set.mem_univ

UniformOnFun

Definitions

Name	Category	Theorems
congrLeft 📖	CompOp	—
congrRight 📖	CompOp	—
gen 📖	CompOp	13 math math: gen_eq_preimage_restrict, hasBasis_uniformity_of_covering_of_basis, uniformity_eq_of_basis, gen_mono, gen_mem_uniformity, hasBasis_nhds_of_basis, hasBasis_uniformity_of_basis, hasBasis_nhds, hasBasis_uniformity_of_basis_aux₁, hasAntitoneBasis_uniformity, uniformity_eq, hasBasis_uniformity, isBasis_gen
ofFun 📖	CompOp	38 math math: UniformConvergenceCLM.isEmbedding_coeFn, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', uniformContinuous_ofUniformFun, ofFun_sum, ofFun_toFun, toFun_ofFun, lipschitzWith_one_ofFun_toFun, EquicontinuousOn.tendsto_uniformOnFun_iff_pi, ContinuousMap.continuous_iff_continuous_uniformOnFun, EquicontinuousOn.inducing_uniformOnFun_iff_pi', ofFun_div, postcomp_uniformContinuous, ofFun_inv, one_apply, postcomp_isUniformInducing, UniformConvergenceCLM.topologicalSpace_eq, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, uniformSpace_eq_iInf_precomp_of_cover, ofFun_sub, UniformConvergenceCLM.isUniformInducing_coeFn, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi, ofFun_prod, precomp_uniformContinuous, UniformConvergenceCLM.uniformSpace_eq, ofFun_mul, uniformSpace_eq_inf_precomp_of_cover, postcomp_isUniformEmbedding, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, ofFun_add, uniformContinuous_ofFun_toFun, ofFun_smul, UniformConvergenceCLM.isUniformEmbedding_coeFn, ofFun_neg, zero_apply, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', lipschitzWith_one_ofFun_toFun'
toFun 📖	CompOp	57 math math: toFun_one, uniformContinuous_eval, ofFun_toFun, isometry_restrict, toFun_ofFun, toFun_neg, isEmbedding_toFun_finite, toFun_div, postcomp_uniformContinuous, lipschitzOnWith_cfc_fun_of_subset, continuousOn_cfc_setProd, tendsto_iff_tendstoUniformlyOn, ContinuousMultilinearMap.range_toUniformOnFun, edist_eval_le, postcomp_isUniformInducing, lipschitzWith_iff, lipschitzOnWith_cfc_fun, continuous_rng_iff, topologicalSpace_eq, uniformSpace_eq_iInf_precomp_of_cover, lipschitzOnWith_cfcₙ_fun, lipschitzWith_eval, ContinuousMap.toUniformOnFun_toFun, uniformContinuous_toFun, continuousOn_eval₂, edist_def', lipschitzOnWith_iff, uniformContinuous_restrict, edist_eq_pi_restrict, edist_def, lipschitzOnWith_cfcₙ_fun_of_subset, toFun_sum, uniformContinuous_restrict_toFun, precomp_uniformContinuous, uniformContinuous_eval_of_mem_sUnion, toFun_sub, isClosed_setOf_continuous, continuousOn_cfcₙ_setProd, ContinuousMultilinearMap.toUniformOnFun_toFun, toFun_add, toFun_inv, uniformSpace_eq_inf_precomp_of_cover, edist_eq_restrict_sUnion, toFun_mul, isUniformEmbedding_toFun_finite, postcomp_isUniformEmbedding, continuousOn_cfc_nnreal_setProd, isUniformInducing_pi_restrict, uniformContinuous_ofFun_toFun, edist_le, uniformContinuous_eval_of_mem, toFun_smul, toFun_prod, continuousOn_cfcₙ_nnreal_setProd, lipschitzWith_restrict, toFun_zero, lipschitzWith_one_ofFun_toFun'
topologicalSpace 📖	CompOp	35 math math: UniformConvergenceCLM.isEmbedding_coeFn, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', EquicontinuousOn.tendsto_uniformOnFun_iff_pi, ContinuousMap.continuous_iff_continuous_uniformOnFun, isEmbedding_toFun_finite, nhds_eq_of_basis, EquicontinuousOn.inducing_uniformOnFun_iff_pi', continuousOn_cfc_setProd, tendsto_iff_tendstoUniformlyOn, continuous_rng_iff, UniformConvergenceCLM.topologicalSpace_eq, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, topologicalSpace_eq, t2Space_of_covering, continuousOn_eval₂, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, hasBasis_nhds_one_of_basis, hasBasis_nhds_zero_of_basis, eVariationOn.lowerSemicontinuous_uniformOn, hasBasis_nhds_of_basis, gen_mem_nhds, isClosed_setOf_continuous, continuousOn_cfcₙ_setProd, hasBasis_nhds_zero, hasBasis_nhds_one, continuousAt_eval₂, continuousOn_cfc_nnreal_setProd, hasBasis_nhds, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, continuousSMul_submodule_of_image_bounded, continuous_of_forall_lipschitzWith, nhds_eq, continuousOn_cfcₙ_nnreal_setProd, eVariationOn.lowerSemicontinuous
uniformEquivPiComm 📖	CompOp	—
uniformEquivProdArrow 📖	CompOp	—
uniformEquivUniformFun 📖	CompOp	—
uniformSpace 📖	CompOp	42 math math: hasBasis_uniformity_of_covering_of_basis, uniformContinuous_ofUniformFun, mono, uniformContinuous_eval, uniformity_eq_of_basis, postcomp_uniformContinuous, isCountablyGenerated_uniformity, instIsUniformGroupUniformOnFun, postcomp_isUniformInducing, instCompleteSpace, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, uniformSpace_eq_iInf_precomp_of_cover, uniformContinuous_toFun, EquicontinuousOn.comap_uniformOnFun_eq, UniformFunOn.uniformContinuousConstSMul, UniformConvergenceCLM.isUniformInducing_coeFn, instIsUniformAddGroupUniformOnFun, uniformContinuous_restrict, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi, gen_mem_uniformity, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, uniformContinuous_restrict_toFun, precomp_uniformContinuous, hasBasis_uniformity_of_basis, uniformContinuous_eval_of_mem_sUnion, UniformConvergenceCLM.uniformSpace_eq, inf_eq, uniformSpace_eq_inf_precomp_of_cover, isUniformEmbedding_toFun_finite, postcomp_isUniformEmbedding, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun, isUniformInducing_pi_restrict, uniformContinuous_ofFun_toFun, uniformContinuous_eval_of_mem, hasAntitoneBasis_uniformity, UniformConvergenceCLM.isUniformEmbedding_coeFn, uniformity_eq, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun, comap_eq, hasBasis_uniformity, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', iInf_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_eq 📖	mathematical	—	uniformSpace UniformSpace.comap	—	UniformSpace.comap_iInf iInf_congr_Prop UniformFun.comap_eq
continuousAt_eval₂ 📖	mathematical	Set Set.instMembership Filter Filter.instMembership nhds ContinuousAt UniformSpace.toTopologicalSpace DFunLike.coe Equiv UniformOnFun EquivLike.toFunLike Equiv.instEquivLike toFun	instTopologicalSpaceProd topologicalSpace	—	ContinuousAt.eq_1 nhds_eq_comap_uniformity Filter.tendsto_comap_iff lift'_comp_uniformity Filter.tendsto_lift' Filter.mp_mem prod_mem_nhds gen_mem_nhds Filter.inter_mem UniformSpace.ball_mem_nhds Filter.univ_mem'
continuousOn_eval₂ 📖	mathematical	Set Set.instMembership Filter Filter.instMembership nhds	ContinuousOn UniformOnFun instTopologicalSpaceProd topologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun setOf ContinuousAt	—	ContinuousAt.continuousWithinAt continuousAt_eval₂
continuous_rng_iff 📖	mathematical	—	Continuous UniformOnFun topologicalSpace UniformFun Set.Elem UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Set.restrict toFun	—	forall_swap
gen_eq_preimage_restrict 📖	mathematical	—	gen Set.preimage UniformFun Set.restrict DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.toFun UniformFun.gen Set.Elem	—	Set.ext
gen_mem_nhds 📖	mathematical	Set Set.instMembership Filter Filter.instMembership uniformity	UniformOnFun nhds topologicalSpace setOf	—	nhds_eq Filter.mem_iInf_of_mem Filter.mem_principal_self
gen_mem_uniformity 📖	mathematical	Set Set.instMembership Filter Filter.instMembership uniformity	UniformOnFun uniformSpace gen	—	uniformity_eq Filter.mem_iInf_of_mem Filter.mem_principal_self
gen_mono 📖	mathematical	Set Set.instHasSubset	UniformOnFun gen	—	—
hasAntitoneBasis_uniformity 📖	mathematical	Set Set.instMembership Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instHasSubset Filter.HasAntitoneBasis uniformity	UniformOnFun uniformSpace gen	—	Filter.HasBasis.nonempty Filter.HasAntitoneBasis.toHasBasis Filter.HasBasis.to_hasBasis hasBasis_uniformity_of_covering_of_basis Monotone.directed_le directed_of gen_mono Filter.HasAntitoneBasis.antitone Set.Subset.rfl
hasBasis_nhds 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset	Filter.HasBasis UniformOnFun nhds topologicalSpace Set.instMembership Filter Filter.instMembership uniformity setOf gen	—	hasBasis_nhds_of_basis Filter.basis_sets
hasBasis_nhds_of_basis 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset Filter.HasBasis uniformity	UniformOnFun nhds topologicalSpace Set.instMembership setOf gen	—	nhds_basis_uniformity hasBasis_uniformity_of_basis
hasBasis_uniformity 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset	Filter.HasBasis UniformOnFun uniformity uniformSpace Set.instMembership Filter Filter.instMembership gen	—	hasBasis_uniformity_of_basis Filter.basis_sets
hasBasis_uniformity_of_basis 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset Filter.HasBasis uniformity	UniformOnFun uniformSpace Set.instMembership gen	—	iInf_uniformity Filter.hasBasis_biInf_of_directed hasBasis_uniformity_of_basis_aux₁ hasBasis_uniformity_of_basis_aux₂
hasBasis_uniformity_of_basis_aux₁ 📖	mathematical	Filter.HasBasis uniformity	UniformOnFun UniformSpace.comap Set.restrict UniformFun.uniformSpace Set.Elem gen	—	gen_eq_preimage_restrict Filter.HasBasis.comap UniformFun.hasBasis_uniformity_of_basis
hasBasis_uniformity_of_basis_aux₂ 📖	mathematical	DirectedOn Set Set.instHasSubset Filter.HasBasis uniformity	Order.Preimage UniformSpace UniformSpace.comap Set.restrict UniformFun.uniformSpace Set.Elem Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace	—	DirectedOn.mono Filter.HasBasis.le_basis_iff hasBasis_uniformity_of_basis_aux₁ gen_mono subset_rfl Set.instReflSubset
hasBasis_uniformity_of_covering_of_basis 📖	mathematical	Set Set.instMembership Directed Set.instHasSubset Filter.HasBasis uniformity	UniformOnFun uniformSpace gen	—	Set.Nonempty.mono Set.range_subset_iff Set.range_nonempty HasSubset.Subset.trans Set.instIsTransSubset Filter.HasBasis.to_hasBasis hasBasis_uniformity_of_basis gen_mono Set.Subset.rfl
iInf_eq 📖	mathematical	—	uniformSpace iInf UniformSpace instInfSetUniformSpace UniformOnFun	—	iInf_congr_Prop UniformFun.iInf_eq UniformSpace.comap_iInf iInf_comm iInf_congr
inf_eq 📖	mathematical	—	uniformSpace UniformSpace instMinUniformSpace UniformOnFun	—	inf_eq_iInf iInf_eq iInf_congr
instCompleteSpace 📖	mathematical	—	CompleteSpace UniformOnFun uniformSpace	—	isEmpty_or_nonempty complete_of_compact Finite.compactSpace Finite.of_subsingleton instSubsingletonUniformOnFun IsEmpty.instSubsingleton CompleteSpace.complete Cauchy.map uniformContinuous_eval_of_mem_sUnion nhds_eq_of_basis uniformity_hasBasis_closed cauchy_iff gen_mem_uniformity Filter.mp_mem Filter.univ_mem' IsClosed.mem_of_tendsto Filter.Tendsto.prodMk_nhds tendsto_const_nhds Set.mk_mem_prod Function.sometimes_spec
isBasis_gen 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset	Filter.IsBasis UniformOnFun Set.instMembership FilterBasis instMembershipSetFilterBasis gen	—	Set.Nonempty.prod FilterBasis.nonempty FilterBasis.inter_sets
isClosed_setOf_continuous 📖	mathematical	Topology.IsCoherentWith	IsClosed UniformOnFun topologicalSpace setOf Continuous UniformSpace.toTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	isClosed_iff_forall_filter Topology.IsCoherentWith.continuous_iff TendstoUniformlyOn.continuousOn tendsto_iff_tendstoUniformlyOn Filter.tendsto_id' Filter.Eventually.frequently Continuous.continuousOn
isCountablyGenerated_uniformity 📖	mathematical	Set Set.instMembership Monotone Nat.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instHasSubset	Filter.IsCountablyGenerated UniformOnFun uniformity uniformSpace	—	Filter.exists_antitone_basis Filter.HasBasis.isCountablyGenerated instCountableNat Filter.HasAntitoneBasis.toHasBasis hasAntitoneBasis_uniformity SemilatticeSup.instIsDirectedOrder
isEmbedding_toFun_finite 📖	mathematical	—	Topology.IsEmbedding UniformOnFun setOf Set Set.Finite topologicalSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_toFun_finite
isUniformEmbedding_toFun_finite 📖	mathematical	—	IsUniformEmbedding UniformOnFun setOf Set Set.Finite uniformSpace Pi.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	Pi.uniformity Filter.comap_iInf Filter.comap_comap Filter.HasBasis.ext Filter.HasBasis.iInf' Filter.HasBasis.comap Filter.basis_sets hasBasis_uniformity Set.finite_empty directedOn_of_sup_mem Set.Finite.union Filter.biInter_mem Set.mem_iInter₂
isUniformInducing_pi_restrict 📖	mathematical	—	IsUniformInducing UniformOnFun uniformSpace Pi.uniformSpace Set.Elem Set UniformFun Set.instMembership UniformFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Set.restrict toFun	—	Pi.uniformSpace_eq UniformSpace.comap_iInf iInf_subtype iInf_congr_Prop
mono 📖	mathematical	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace Set Set.instHasSubset	UniformOnFun uniformSpace	—	iInf_le_iInf_of_subset iInf₂_mono UniformSpace.comap_mono UniformFun.mono
nhds_eq 📖	mathematical	—	nhds UniformOnFun topologicalSpace iInf Filter Set Filter.instInfSet Set.instMembership Filter.instMembership uniformity Filter.principal setOf	—	nhds_eq_of_basis Filter.basis_sets
nhds_eq_of_basis 📖	mathematical	Filter.HasBasis uniformity	nhds UniformOnFun topologicalSpace iInf Filter Set Filter.instInfSet Set.instMembership Filter.principal setOf	—	nhds_eq_comap_uniformity uniformity_eq_of_basis Filter.comap_iInf iInf_congr_Prop Filter.comap_principal
ofFun_toFun 📖	mathematical	—	DFunLike.coe Equiv UniformOnFun EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	—
postcomp_isUniformEmbedding 📖	mathematical	IsUniformEmbedding	UniformOnFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	postcomp_isUniformInducing IsUniformEmbedding.isUniformInducing IsUniformEmbedding.injective
postcomp_isUniformInducing 📖	mathematical	IsUniformInducing	UniformOnFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	IsUniformInducing.comap_uniformity uniformity_comap UniformSpace.ext comap_eq
postcomp_uniformContinuous 📖	mathematical	UniformContinuous	UniformOnFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	uniformContinuous_iff LE.le.trans_eq mono subset_rfl Set.instReflSubset comap_eq
precomp_uniformContinuous 📖	mathematical	Set.MapsTo Set Set.image	UniformContinuous UniformOnFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	uniformity_eq Filter.tendsto_iInf' Set.forall_mem_image
t2Space_of_covering 📖	mathematical	Set.sUnion Set.univ	T2Space UniformOnFun topologicalSpace	—	Set.mem_sUnion separated_by_continuous UniformContinuous.continuous uniformContinuous_eval_of_mem
tendsto_iff_tendstoUniformlyOn 📖	mathematical	—	Filter.Tendsto UniformOnFun nhds topologicalSpace TendstoUniformlyOn DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	nhds_eq
toFun_ofFun 📖	mathematical	—	DFunLike.coe Equiv UniformOnFun EquivLike.toFunLike Equiv.instEquivLike toFun ofFun	—	—
topologicalSpace_eq 📖	mathematical	—	topologicalSpace iInf TopologicalSpace UniformOnFun Set ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.instMembership TopologicalSpace.induced UniformFun Set.Elem DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Set.restrict toFun UniformFun.topologicalSpace	—	UniformSpace.toTopologicalSpace_iInf
uniformContinuous_eval 📖	mathematical	Set.sUnion Set.univ	UniformContinuous UniformOnFun uniformSpace Function.eval DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	uniformContinuous_eval_of_mem_sUnion Set.mem_univ
uniformContinuous_eval_of_mem 📖	mathematical	Set Set.instMembership	UniformContinuous UniformOnFun uniformSpace Function.eval DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	UniformContinuous.comp UniformFun.uniformContinuous_eval uniformContinuous_restrict
uniformContinuous_eval_of_mem_sUnion 📖	mathematical	Set Set.instMembership Set.sUnion	UniformContinuous UniformOnFun uniformSpace Function.eval DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	uniformContinuous_eval_of_mem
uniformContinuous_ofFun_toFun 📖	mathematical	Set Set.instHasSubset Set.Finite Set.sUnion	UniformContinuous UniformOnFun uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	uniformity_eq iInf₂_comm Filter.tendsto_iInf_iInf Set.mem_sUnion Set.iInter_congr_Prop
uniformContinuous_ofUniformFun 📖	mathematical	—	UniformContinuous UniformFun UniformOnFun UniformFun.uniformSpace uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun UniformFun.toFun	—	uniformity_eq Filter.HasBasis.eventually_iff UniformFun.hasBasis_uniformity
uniformContinuous_restrict 📖	mathematical	Set Set.instMembership	UniformContinuous UniformOnFun UniformFun Set.Elem uniformSpace UniformFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Set.restrict toFun	—	iInf_uniformity iInf₂_le
uniformContinuous_restrict_toFun 📖	mathematical	—	UniformContinuous UniformOnFun uniformSpace Pi.uniformSpace Set.Elem Set.sUnion Set.restrict DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	uniformContinuous_pi Set.mem_sUnion uniformContinuous_eval_of_mem
uniformContinuous_toFun 📖	mathematical	Set.sUnion Set.univ	UniformContinuous UniformOnFun uniformSpace Pi.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toFun	—	uniformContinuous_pi uniformContinuous_eval
uniformSpace_eq_iInf_precomp_of_cover 📖	mathematical	Set.MapsTo Set Set.image Set.preimage Set.Finite Set.instHasSubset Set.iUnion Set.instMembership Set.range	uniformSpace iInf UniformSpace UniformOnFun instInfSetUniformSpace UniformSpace.comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	UniformFun.uniformSpace_eq_iInf_precomp_of_cover Set.iUnion_congr_Prop Set.range_restrictPreimage Set.image_univ Subtype.range_val le_antisymm le_iInf uniformContinuous_iff precomp_uniformContinuous le_iInf₂ UniformSpace.comap_iInf iInf_congr_Prop iInf_mono iInf₂_le_of_le le_rfl
uniformSpace_eq_inf_precomp_of_cover 📖	mathematical	Set.MapsTo Set Set.image Set.preimage Set.instHasSubset Set.instUnion Set.range	uniformSpace UniformSpace UniformOnFun instMinUniformSpace UniformSpace.comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun toFun	—	UniformFun.uniformSpace_eq_inf_precomp_of_cover Set.range_restrictPreimage Set.image_univ Subtype.range_val le_antisymm le_inf uniformContinuous_iff precomp_uniformContinuous le_iInf₂ UniformSpace.comap_iInf UniformSpace.comap_inf iInf_congr_Prop inf_le_inf iInf₂_le_of_le le_rfl
uniformity_eq 📖	mathematical	—	uniformity UniformOnFun uniformSpace iInf Filter Set Filter.instInfSet Set.instMembership Filter.instMembership Filter.principal gen	—	uniformity_eq_of_basis Filter.basis_sets
uniformity_eq_of_basis 📖	mathematical	Filter.HasBasis uniformity	UniformOnFun uniformSpace iInf Filter Set Filter.instInfSet Set.instMembership Filter.principal gen	—	iInf_uniformity iInf_congr_Prop Filter.HasBasis.eq_biInf UniformFun.hasBasis_uniformity_of_basis Filter.comap_iInf Filter.comap_principal

(root)

Definitions

Name	Category	Theorems
UniformFun 📖	CompOp	94 math math: Equicontinuous.inducing_uniformFun_iff_pi, UniformOnFun.gen_eq_preimage_restrict, UniformFun.ofFun_one, UniformFun.edist_eval_le, UniformOnFun.uniformContinuous_ofUniformFun, UniformOnFun.isometry_restrict, UniformFun.uniformSpace_eq_iInf_precomp_of_cover, UniformFun.toFun_sub, UniformOnFun.lipschitzWith_one_ofFun_toFun, UniformFun.toFun_ofFun, instIsUniformAddGroupUniformFun, BoundedContinuousFunction.isEmbedding_coeFn, UniformFun.mono, UniformFun.hasBasis_nhds_zero_of_basis, UniformFun.hasBasis_uniformity, Equicontinuous.tendsto_uniformFun_iff_pi, equicontinuousWithinAt_iff_continuousWithinAt, UniformFun.postcomp_isUniformInducing, UniformFun.hasBasis_nhds_zero, UniformFun.toFun_zero, UniformFun.instT2Space, UniformFun.instCompleteSpace, UniformFun.isometry_ofFun_continuousMap, UniformFun.tendsto_iff_tendstoUniformly, instNonemptyUniformFun, equicontinuousOn_iff_continuousOn, instIsScalarTowerUniformFun, UniformOnFun.continuous_rng_iff, UniformFun.isometry_ofFun_boundedContinuousFunction, UniformFun.toFun_smul, UniformFun.ofFun_zero, UniformFun.ofFun_div, UniformFun.instBoundedSpace, UniformFun.edist_le, instSMulCommClassUniformFun, UniformOnFun.topologicalSpace_eq, UniformFun.toFun_one, UniformFun.hasBasis_nhds_one_of_basis, UniformFun.lipschitzWith_ofFun_iff, UniformFun.toFun_prod, equicontinuous_iff_continuous, ContinuousMap.continuous_iff_continuous_uniformFun, UniformFun.hasBasis_uniformity_of_basis, UniformFun.toFun_div, UniformFun.dist_le, UniformFun.ofFun_smul, UniformFun.precomp_uniformContinuous, Equicontinuous.isUniformInducing_uniformFun_iff_pi, UniformFun.ofFun_prod, UniformFun.postcomp_uniformContinuous, UniformFun.edist_def, UniformFun.ofFun_neg, UniformOnFun.uniformContinuous_restrict, UniformFun.hasBasis_nhds_one, UniformOnFun.edist_eq_pi_restrict, uniformEquicontinuousOn_iff_uniformContinuousOn, UniformFun.lipschitzWith_iff, UniformFun.mem_gen, UniformFun.toFun_neg, ContinuousMap.isUniformEmbedding_uniformFunOfFun, UniformFun.isBasis_gen, instIsUniformGroupUniformFun, UniformFun.toFun_add, UniformFun.uniformContinuous_eval, UniformFun.lipschitzOnWith_ofFun_iff, UniformFun.ofFun_sub, equicontinuousAt_iff_continuousAt, UniformOnFun.edist_eq_restrict_sUnion, UniformFun.uniformContinuous_toFun, UniformFun.toFun_inv, UniformFun.uniformContinuousConstSMul, UniformFun.ofFun_sum, UniformFun.toFun_sum, UniformFun.ofFun_add, UniformFun.ofFun_toFun, UniformFun.iInf_eq, UniformOnFun.isUniformInducing_pi_restrict, UniformFun.uniformSpace_eq_inf_precomp_of_cover, UniformFun.dist_def, UniformFun.gc, UniformFun.toFun_mul, UniformFun.postcomp_isUniformEmbedding, UniformFun.lipschitzOnWith_iff, UniformOnFun.lipschitzWith_restrict, instSubsingletonUniformFun, UniformFun.hasBasis_nhds_of_basis, UniformFun.inf_eq, UniformFun.ofFun_mul, UniformFun.hasBasis_nhds, uniformEquicontinuous_iff_uniformContinuous, UniformFun.isClosed_setOf_continuous, BoundedContinuousFunction.isInducing_coeFn, UniformFun.ofFun_inv, UniformFun.lipschitzWith_eval
UniformOnFun 📖	CompOp	126 math math: UniformConvergenceCLM.isEmbedding_coeFn, UniformOnFun.toFun_one, UniformOnFun.instBoundedSpace, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', UniformOnFun.hasBasis_uniformity_of_covering_of_basis, UniformOnFun.uniformContinuous_ofUniformFun, UniformOnFun.mono, UniformOnFun.ofFun_sum, UniformOnFun.uniformContinuous_eval, UniformOnFun.ofFun_toFun, UniformOnFun.uniformity_eq_of_basis, UniformOnFun.isometry_restrict, UniformOnFun.gen_mono, UniformOnFun.toFun_ofFun, UniformOnFun.toFun_neg, UniformOnFun.lipschitzWith_one_ofFun_toFun, EquicontinuousOn.tendsto_uniformOnFun_iff_pi, ContinuousMap.continuous_iff_continuous_uniformOnFun, UniformOnFun.isEmbedding_toFun_finite, UniformOnFun.nhds_eq_of_basis, UniformOnFun.toFun_div, EquicontinuousOn.inducing_uniformOnFun_iff_pi', UniformOnFun.ofFun_div, UniformOnFun.postcomp_uniformContinuous, instSubsingletonUniformOnFun, UniformOnFun.ofFun_inv, lipschitzOnWith_cfc_fun_of_subset, continuousOn_cfc_setProd, UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformOnFun.isCountablyGenerated_uniformity, instIsUniformGroupUniformOnFun, ContinuousMultilinearMap.range_toUniformOnFun, UniformOnFun.one_apply, UniformOnFun.edist_eval_le, UniformOnFun.postcomp_isUniformInducing, instSMulCommClassUniformOnFun, UniformOnFun.instCompleteSpace, instIsScalarTowerUniformOnFun, UniformOnFun.lipschitzWith_iff, lipschitzOnWith_cfc_fun, UniformOnFun.continuous_rng_iff, UniformConvergenceCLM.topologicalSpace_eq, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, UniformOnFun.topologicalSpace_eq, UniformOnFun.t2Space_of_covering, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, UniformOnFun.ofFun_sub, lipschitzOnWith_cfcₙ_fun, instNonemptyUniformOnFun, UniformOnFun.lipschitzWith_eval, ContinuousMap.toUniformOnFun_toFun, UniformOnFun.uniformContinuous_toFun, UniformOnFun.continuousOn_eval₂, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, UniformOnFun.edist_def', UniformFunOn.uniformContinuousConstSMul, UniformConvergenceCLM.isUniformInducing_coeFn, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, instIsUniformAddGroupUniformOnFun, UniformOnFun.lipschitzOnWith_iff, UniformOnFun.hasBasis_nhds_one_of_basis, UniformOnFun.uniformContinuous_restrict, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi, UniformOnFun.gen_mem_uniformity, UniformOnFun.edist_eq_pi_restrict, UniformOnFun.edist_def, lipschitzOnWith_cfcₙ_fun_of_subset, UniformOnFun.ofFun_prod, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, UniformOnFun.hasBasis_nhds_zero_of_basis, UniformOnFun.toFun_sum, UniformOnFun.uniformContinuous_restrict_toFun, UniformOnFun.precomp_uniformContinuous, eVariationOn.lowerSemicontinuous_uniformOn, UniformOnFun.hasBasis_nhds_of_basis, UniformOnFun.hasBasis_uniformity_of_basis, UniformOnFun.uniformContinuous_eval_of_mem_sUnion, UniformOnFun.toFun_sub, UniformOnFun.gen_mem_nhds, UniformOnFun.isClosed_setOf_continuous, continuousOn_cfcₙ_setProd, ContinuousMultilinearMap.toUniformOnFun_toFun, UniformConvergenceCLM.uniformSpace_eq, UniformOnFun.toFun_add, UniformOnFun.hasBasis_nhds_zero, UniformOnFun.inf_eq, UniformOnFun.toFun_inv, UniformOnFun.ofFun_mul, UniformOnFun.hasBasis_nhds_one, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, UniformOnFun.edist_eq_restrict_sUnion, UniformOnFun.toFun_mul, UniformOnFun.isUniformEmbedding_toFun_finite, UniformOnFun.postcomp_isUniformEmbedding, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun, continuousOn_cfc_nnreal_setProd, UniformOnFun.hasBasis_nhds, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, UniformOnFun.continuousSMul_submodule_of_image_bounded, UniformOnFun.ofFun_add, UniformOnFun.isUniformInducing_pi_restrict, UniformOnFun.uniformContinuous_ofFun_toFun, UniformOnFun.edist_le, ContinuousMap.range_toUniformOnFunIsCompact, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, UniformOnFun.uniformContinuous_eval_of_mem, UniformOnFun.nhds_eq, UniformOnFun.hasAntitoneBasis_uniformity, UniformOnFun.toFun_smul, UniformOnFun.ofFun_smul, UniformOnFun.toFun_prod, UniformConvergenceCLM.isUniformEmbedding_coeFn, continuousOn_cfcₙ_nnreal_setProd, eVariationOn.lowerSemicontinuous, UniformOnFun.uniformity_eq, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun, UniformOnFun.ofFun_neg, UniformOnFun.lipschitzWith_restrict, UniformOnFun.hasBasis_uniformity, UniformOnFun.zero_apply, UniformOnFun.toFun_zero, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', UniformOnFun.isBasis_gen, UniformOnFun.lipschitzWith_one_ofFun_toFun', UniformOnFun.iInf_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyUniformFun 📖	mathematical	—	UniformFun	—	—
instNonemptyUniformOnFun 📖	mathematical	—	UniformOnFun	—	—
instSubsingletonUniformFun 📖	mathematical	—	UniformFun	—	—
instSubsingletonUniformOnFun 📖	mathematical	—	UniformOnFun	—	—

---

← Back to Index