Semantic Mathlib search

Describe the result you need.

Search 310,579 declarations by meaning, plus 10,000 selected theorems with exact statements and source links from a separate pinned Mathlib revision.

Pinned Mathlib source

2 exact-source matches

10,000 complete declarations

Source result 1 · theorem

BoundedContinuousFunction.arzela_ascoli

Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean:109 to 119 · bbc4475e9e8f · Apache-2.0

Exact source

Exact Lean statement

theorem arzela_ascoli [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)) (in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) : IsCompact (closure A)

Source result 2 · theorem

BoundedContinuousFunction.arzela_ascoli₁

Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean:30 to 87 · bbc4475e9e8f · Apache-2.0

Exact source

Exact Lean statement

theorem arzela_ascoli₁ [CompactSpace β] (A : Set (α →ᵇ β)) (closed : IsClosed A) (H : Equicontinuous ((↑) : A → α → β)) : IsCompact A

These records preserve the complete declaration, pinned commit, exact source range, and Apache-2.0 license. They do not infer individual authorship or independent verification.

Mathlib v4.28.0-rc1

5 semantic matches

Open in LeanSearch

Result 1 · theorem

IsCompact.exists_bound_of_continuousOn

Mathlib.Analysis.Normed.Group.Bounded

Mathlib docs

What it says

Existence of a Bound for Continuous Functions on Compact Sets in Seminormed Additive Groups

If s s is a compact subset of a topological space α \alpha and f:αE f : \alpha \to E is a function that is continuous on s s , where E E is a seminormed additive group, then there exists a real constant C C such that f(x)C \|f(x)\| \leq C for all xs x \in s . This establishes that continuous functions on compact sets are bounded in seminormed additive groups.

Result 2 · theorem

IsCompact.exists_bound_of_continuousOn'

Mathlib.Analysis.Normed.Group.Bounded

Mathlib docs

What it says

Boundedness of Continuous Functions on Compact Sets

For any topological space α\alpha and compact subset sαs \subseteq \alpha, if f:αEf : \alpha \to E is a function continuous on ss (where EE is a seminormed group), then there exists a real number CC such that f(x)C\|f(x)\| \leq C for all xsx \in s.

Result 3 · definition

BoundedContinuousFunction.mkOfCompact

Mathlib.Topology.ContinuousMap.Bounded.Basic

Mathlib docs

What it says

Bounded continuous function from compact space

Given a compact topological space α\alpha and a continuous function f:αβf : \alpha \to \beta where β\beta is a pseudo-metric space, this constructs the corresponding bounded continuous function. The image of α\alpha under ff is compact (hence bounded) in β\beta by continuity, so no explicit bound is required.

Result 4 · theorem

ContinuousMap.apply_le_norm

Mathlib.Topology.ContinuousMap.Compact

Mathlib docs

What it says

Continuous Function on Compact Space is Bounded by Its Supremum Norm

For any continuous function f f from a compact topological space α \alpha to the real numbers R \mathbb{R} , and for every point xα x \in \alpha , it holds that f(x)f f(x) \leq \|f\| , where f \|f\| denotes the supremum norm of f f , defined as the supremum of f(x) |f(x)| over all xα x \in \alpha .

Result 5 · theorem

HasCompactSupport.exists_bound_of_continuous

Mathlib.Analysis.Normed.Group.Bounded

Mathlib docs

What it says

Boundedness of Continuous Functions with Compact Support

If a function f:αE f : \alpha \to E is continuous and has compact support, then there exists a constant C C such that f(x)C \|f(x)\| \leq C for all xα x \in \alpha .

These are federated discovery results from a published Apache-2.0 corpus. They are not Therefore proof records, independent rebuilds, axiom audits, or authorship claims.