ArzelaAscoli

📁 Source: Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean

Statistics

Metric	Count
Definitions	0
Theorems arzela_ascoli, arzela_ascoli₁, arzela_ascoli₂	3
Total	3

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arzela_ascoli 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Set Set.instMembership DFunLike.coe BoundedContinuousFunction instFunLike Equicontinuous Set.Elem	instPseudoMetricSpace closure	—	arzela_ascoli₂ isClosed_closure Metric.mem_of_closed' IsCompact.isClosed Metric.mem_closure_iff lt_of_le_of_lt dist_coe_le_dist Equicontinuous.closure' continuous_coe
arzela_ascoli₁ 📖	mathematical	Equicontinuous Set.Elem BoundedContinuousFunction PseudoMetricSpace.toUniformSpace DFunLike.coe instFunLike Set Set.instMembership	IsCompact UniformSpace.toTopologicalSpace instPseudoMetricSpace	—	TotallyBounded.isCompact_of_isClosed instCompleteSpace complete_of_proper proper_of_compact Metric.totallyBounded_of_finite_discretization exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat half_pos mem_nhds_iff IsCompact.elim_finite_subcover_image isCompact_univ Set.mem_biUnion Set.mem_univ Set.Finite.nonempty_fintype finite_cover_balls_of_compact lt_of_le_of_lt dist_le le_of_lt Set.mem_iUnion₂ dist_triangle4_right add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add dist_triangle_right add_halves CharZero.NeZero.two IsStrictOrderedRing.toCharZero
arzela_ascoli₂ 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Set Set.instMembership DFunLike.coe BoundedContinuousFunction instFunLike Equicontinuous Set.Elem	instPseudoMetricSpace	—	LipschitzWith.subtype_val IsCompact.of_isClosed_subset IsCompact.image arzela_ascoli₁ isCompact_iff_compactSpace continuous_iff_isClosed continuous_comp IsUniformInducing.equicontinuous_iff IsUniformEmbedding.isUniformInducing isUniformEmbedding_subtype_val Equicontinuous.comp ext

---

← Back to Index