Theorems · Inductive type · general topology

Function.locallyFinsuppWithin

{X : Type u_1} → [TopologicalSpace X] → Set X → (Y : Type u_2) → [Zero Y] → Type (max u_1 u_2)

A function with locally finite support within U is a triple as specified below.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

127 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

TopologicalSpaceZero