app_eq_invApp_app_of_comp_eq_aux — Mathlib

English

Open immersions are stable under composition; if f and g are open immersions, so is their composition.

Русский

Открытые вложения устойчивы к композиции; если f и g — открытые вложения, то и их композиция открытое вложение.

LaTeX

$$$ \text{IsOpenImmersion}(f) \wedge \text{IsOpenImmersion}(g) \Rightarrow \text{IsOpenImmersion}(g \circ f)$$$

Lean4

theorem app_eq_invApp_app_of_comp_eq_aux {X Y U : Scheme.{u}} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = f ≫ g)
    [h : IsOpenImmersion g] (V : U.Opens) : f ⁻¹ᵁ V = fg ⁻¹ᵁ (g ''ᵁ V) := by simp_all

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