ι_toIso_inv — Mathlib

English

The inclusion ι from the top open into X composed with the inverse of the top iso yields the identity on the top open; i.e., Opens.ι ≫ X.topIso.inv = 1.

Русский

Включение ι сверху в X композиционно с обратной стороны топ-изоморфизма даёт тождество на ⊤.

LaTeX

$$$ Opens.\\iota \\circ X.topIso.inv = 1$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_toIso_inv (X : Scheme.{u}) : Opens.ι _ ≫ X.topIso.inv = 𝟙 _ :=
  X.topIso.hom_inv_id

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