opensRange_comp — Mathlib

English

If f is an isomorphism, then f.opensRange equals the top open set.

Русский

Если f является изоморфизмом, то f.opensRange равен верхнему открытому множеству.

LaTeX

$$$f.opensRange = \\top$ when $f$ is an isomorphism$$

Lean4

theorem opensRange_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] :
    (f ≫ g).opensRange = g ''ᵁ f.opensRange :=
  TopologicalSpace.Opens.ext (Set.range_comp g.base f.base)

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