comp_iff

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsDominant.comp_iff

English

If f is dominant, then IsDominant(f ≫ g) holds if and only if IsDominant(g).

Русский

Если f доминирует, то IsDominant(f ≫ g) эквивалентно IsDominant(g).

LaTeX

$$$\\mathrm{IsDominant}(f) \\Rightarrow (\\mathrm{IsDominant}(f \\circ g) \\Leftrightarrow \\mathrm{IsDominant}(g))$$$

Lean4

theorem comp_iff [IsDominant f] : IsDominant (f ≫ g) ↔ IsDominant g :=
  ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru