comp — Mathlib

English

If g and f are conformal maps, then their composition g ∘ f is conformal.

Русский

Если g и f конформны, то их композиция g ∘ f конформна.

LaTeX

$$$IsConformalMap g\to IsConformalMap f\to IsConformalMap (g \circ f)$$$

Lean4

theorem comp (hg : IsConformalMap g) (hf : IsConformalMap f) : IsConformalMap (g.comp f) :=
  by
  rcases hf with ⟨cf, hcf, lif, rfl⟩
  rcases hg with ⟨cg, hcg, lig, rfl⟩
  refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, ?_⟩
  rw [smul_comp, comp_smul, mul_smul]
  rfl

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