Theorems · Inductive type · category theory

TopCat.LocalPredicate

{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 : LocalPredicate 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, and * a proof that given some f : Π x : U, T x, if for every x : U we can find an open set x ∈ V ≤ U so that the restriction of f to V satisfies the predicate, then f itself satisfies the predicate.

Defined in

Mathlib.Topology.Sheaves.LocalPredicate

Cited by

10 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms