congr_germ — Mathlib

English

If two functions f and g are eventually equal along l', then composing with φ gives equal germs when φ tends to l.

Русский

Если две функции f и g равны почти повсюду по l', то их композиции с φ дают равные зародыши при сходимости φ к l.

LaTeX

$$$ h : f =^\!*[l'] g \Rightarrow \forall \phi, \ Tendsto \phi \ l \ l' \Rightarrow (f \circ \phi : \mathrm{Germ}(l, \gamma)) = g \circ \phi $$$

Lean4

theorem congr_germ {f g : β → γ} {l : Filter α} {l' : Filter β} (h : f =ᶠ[l'] g) {φ : α → β} (hφ : Tendsto φ l l') :
    (f ∘ φ : Germ l γ) = g ∘ φ :=
  EventuallyEq.germ_eq (h.comp_tendsto hφ)

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