forall_restrictGermPredicate_of_forall

English

If for every x, P x (f) holds as a germ, then RestrictGermPredicate P A x f holds for every x.

Русский

Если для каждого x выполняется P x (f) в виде гёрма, тогда ограниченный предикат держится для каждого x.

LaTeX

$$$(\forall x, P x (\mathrm{Germ.ofFun} f)) \Rightarrow \forall x, \ RestrictGermPredicate P A x (\mathrm{Germ.ofFun} f)$$$

Lean4

theorem forall_restrictGermPredicate_of_forall {P : ∀ x : X, Germ (𝓝 x) Y → Prop} (h : ∀ x, P x f) :
    ∀ x, RestrictGermPredicate P A x f :=
  forall_restrictGermPredicate_iff.mpr (Eventually.of_forall h)

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