Theorems · Definition · general topology

PiNat.res

{α : Type u_2} → (ℕ → α) → ℕ → List α

In the case where E has constant value α, the cylinder cylinder x n can be identified with the element of List α consisting of the first n entries of x. See cylinder_eq_res. We call this list res x n, the restriction of x to n.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

12 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms