English
Let P assign a predicate to germs P(x, φ) for each x. For a subset A ⊆ X, RestrictGermPredicate P A is the corresponding restricted predicate on germs, defined so that for any function f, RestrictGermPredicate P A x f holds exactly when x ∈ A implies ∀ near x, P y f.
Русский
Пусть P задаёт предикат на гёрмах: для каждой x предикат P x φ. Для множества A ⊆ X определяется ограниченный предикат RestrictGermPredicate P A на гёрмах так, что для любой функции f выполнение предиката на точке x эквивалентно тому, что если x ∈ A, то в окрестности x выполняется P.
LaTeX
$$$(\forall x, \text{RestrictGermPredicate } P A x f) \iff (x \in A \Rightarrow \forall^\infty y \in 𝓝 x, P y f)$$$
Lean4
/-- Given a predicate on germs `P : Π x : X, germ (𝓝 x) Y → Prop` and `A : set X`,
build a new predicate on germs `RestrictGermPredicate P A` such that
`(∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x near A, P x f`, see
`forall_restrictGermPredicate_iff` for this equivalence. -/
def RestrictGermPredicate (P : ∀ x : X, Germ (𝓝 x) Y → Prop) (A : Set X) : ∀ x : X, Germ (𝓝 x) Y → Prop := fun x φ ↦
Germ.liftOn φ (fun f ↦ x ∈ A → ∀ᶠ y in 𝓝 x, P y f)
haveI : ∀ f f' : X → Y, f =ᶠ[𝓝 x] f' → (∀ᶠ y in 𝓝 x, P y f) → ∀ᶠ y in 𝓝 x, P y f' :=
by
intro f f' hff' hf
apply (hf.and <| Eventually.eventually_nhds hff').mono
rintro y ⟨hy, hy'⟩
rwa [Germ.coe_eq.mpr (EventuallyEq.symm hy')]
fun f f' hff' ↦ propext <| forall_congr' fun _ ↦ ⟨this f f' hff', this f' f hff'.symm⟩
