Theorems · Definition · general topology

Filter.Germ

{α : Type u_1} → Filter α → Type u_5 → Type (max u_1 u_5)

The space of germs of functions α → β at a filter l.

Defined in

Mathlib.Order.Filter.Germ.Basic

Cited by

102 results in Mathlib

Foundations

Depth 16 from the axioms, rests on 34 definitions · uses no axioms