congr — Mathlib

English

If f is conformal at x and g agrees with f on an open neighborhood within an open set u containing x, then g is conformal at x.

Русский

Если f конформна в x и g совпадает с f на окрестности x внутри открытого множества u, то g конформна в x.

LaTeX

$$$x\\in u \\wedge IsOpen(u) \\wedge \\operatorname{ConformalAt}(f,x) \\wedge (\\forall y\\in u, g(y)=f(y)) \\Rightarrow \\operatorname{ConformalAt}(g,x)$$$

Lean4

theorem congr {f g : X → Y} {x : X} {u : Set X} (hx : x ∈ u) (hu : IsOpen u) (hf : ConformalAt f x)
    (h : ∀ x : X, x ∈ u → g x = f x) : ConformalAt g x :=
  let ⟨f', hfderiv, hf'⟩ := hf
  ⟨f', hfderiv.congr_of_eventuallyEq ((hu.eventually_mem hx).mono h), hf'⟩

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