van_kampen' — Mathlib

English

In an adhesive category, for a pushout F, if g is mono, then the pushout is van Kampen; equivalently, van_kampen' reduces to van_kampen on the flipped square.

Русский

В адгезивной категории, для pushout-фигуры F, если g моно, то эта вещь ван-Кемпен; эквивалентно переходу к ван-Кемпен для перевёрнутого квадрата.

LaTeX

$$$[Adhesive\ C] [Mono\ g] (H : IsPushout f g h i) : H.IsVanKampen$$

Lean4

theorem van_kampen' [Adhesive C] [Mono g] (H : IsPushout f g h i) : H.IsVanKampen :=
  (Adhesive.van_kampen H.flip).flip

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