Theorems · Theorem · category theory

TopCat.LocalPredicate.locality

∀ {X : TopCat} {T : ↑X → Type u_1} (self : TopCat.LocalPredicate T) {U : TopologicalSpace.Opens ↑X}
  (f : (x : ↥U) → T ↑x), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, self.pred fun x => f (i x)) → self.pred f

A local predicate must be local provided that it is locally satisfied, it is also globally satisfied

Defined in

Mathlib.Topology.Sheaves.LocalPredicate

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound