comp — Mathlib

English

If f is conformal at x and g is conformal at f(x), then the composition g ∘ f is conformal at x.

Русский

Если f конформна в x, а g конформна в f(x), то композиция g ∘ f конформна в x.

LaTeX

$$$\\operatorname{ConformalAt}(f,x) \\wedge \\operatorname{ConformalAt}(g, f(x)) \\Rightarrow \\operatorname{ConformalAt}(g \\circ f, x)$$$

Lean4

theorem comp {f : X → Y} {g : Y → Z} (x : X) (hg : ConformalAt g (f x)) (hf : ConformalAt f x) :
    ConformalAt (g ∘ f) x := by
  rcases hf with ⟨f', hf₁, cf⟩
  rcases hg with ⟨g', hg₁, cg⟩
  exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩

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