forall_restrictGermPredicate_iff — Mathlib

English

For any P and A, the family of restricted germs is equivalent to P holding near A; i.e., (∀ x, RestrictGermPredicate P A x f) is equivalent to ∀ᶠ x in 𝓝ˢ A, P x f.

Русский

Для любых P и A множество ограниченных гёрмов эквивалентно тому, что P выполняется в окрестности A; то есть (∀ x, RestrictGermPredicate P A x f) эквивалентно ∀ᶠ x в 𝓝ˢ A, P x f.

LaTeX

$$$\bigl(\forall x, \text{RestrictGermPredicate } P A x f\bigr) \ ;\iff\; \bigl(\forall^\infty x \in 𝓝^s A, P x f\bigr)$$$

Lean4

theorem forall_restrictGermPredicate_iff {P : ∀ x : X, Germ (𝓝 x) Y → Prop} :
    (∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x in 𝓝ˢ A, P x f :=
  by
  rw [eventually_nhdsSet_iff_forall]
  rfl

Похожие утверждения