comp₂_toGerm — Mathlib

English

The germ of comp₂ g hg f₁ f₂ is the germ of the two inputs mapped via g, i.e., f₁.toGerm.map₂ g f₂.toGerm.

Русский

Гарм comp₂g hg f₁ f₂ равен гарм, полученным отображением двух входов через g: f₁.toGerm.map₂ g f₂.toGerm.

LaTeX

$$$(comp₂ g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm$$$

Lean4

theorem comp₂_toGerm (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    (comp₂ g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm :=
  induction_on₂ f₁ f₂ fun f₁ _ f₂ _ => by simp

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