isoOfLE_inv_ι — Mathlib

English

For opens U ≤ V, the inverse map satisfies (Scheme.Opens.isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι; showing the inverse respects inclusions.

Русский

Для U ≤ V: (Scheme.Opens.isoOfLE hUV).inv ∘ (V.ι ⁻¹ᵁ U).ι ∘ V.ι = U.ι

LaTeX

$$(Scheme.Opens.isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfLE_inv_ι {X : Scheme.{u}} {U V : X.Opens} (hUV : U ≤ V) :
    (Scheme.Opens.isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι := by simp [isoOfLE]

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