hasPushout_symmetry — Mathlib

English

If the pushout of f and g exists, then the pushout of g and f also exists, with a canonical symmetry isomorphism exchanging the legs.

Русский

Если существует пушаут для f и g, то существует пушаут для g и f с каноническим изоморфизмом, обменивающим стороны.

LaTeX

$$$$ \text{HasPushout}(f,g) \Rightarrow \text{HasPushout}(g,f). $$$$

Lean4

/-- Making this a global instance would make the typeclass search go in an infinite loop. -/
theorem hasPushout_symmetry [HasPushout f g] : HasPushout g f :=
  ⟨⟨⟨_, PushoutCocone.flipIsColimit (pushoutIsPushout f g)⟩⟩⟩

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