Theorems · Inductive type · category theory

TopCat.PrelocalPredicate

{X : TopCat} → (↑X → Type u_1) → Type (max u_1 u_2)

Given a topological space X : TopCat and a type family T : X → Type, a P : PrelocalPredicate T consists of: * a family of predicates P.pred, one for each U : Opens X, of the form (Π x : U, T x) → Prop * a proof that if f : Π x : V, T x satisfies the predicate on V : Opens X, then the restriction of f to any open subset U also satisfies the predicate.

Defined in

Mathlib.Topology.Sheaves.LocalPredicate

Cited by

15 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms