comp_iff — Mathlib

English

For morphisms f,g with [IsImmersion g], IsImmersion(f ≫ g) iff IsImmersion f.

Русский

Для морфизмов f,g со _IsImmersion g_ имеем: IsImmersion(f ≫ g) эквивалентно IsImmersion f.

LaTeX

$$$\\text{IsImmersion}(f \\circ g) \\iff \\text{IsImmersion}(f)$$$

Lean4

theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion g] : IsImmersion (f ≫ g) ↔ IsImmersion f :=
  ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

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