iso_hom_base_inv_base — Mathlib

English

For an isomorphism e: X ≅ Y and a point x ∈ X, the composite of the inverse base map with the forward base map returns x.

Русский

Для изоморфизма e: X ≅ Y и точки x ∈ X композиция обратного базового отображения и прямого базового отображения возвращает x.

LaTeX

$$$$e.inv.base (e.hom.base x) = x.$$$$

Lean4

@[simp]
theorem iso_hom_base_inv_base {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) : e.hom.base ≫ e.inv.base = 𝟙 _ :=
  by
  rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_toShHom]
  simp

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