equalizerIso_inv_comp_ι — Mathlib

English

There is an equivalence between Nonempty IsLimit (Fork.ofι f w) and the universal property: ∀ y, g y = h y → ∃! x : X, f x = y.

Русский

Существуют эквивалентности между не пустым IsLimit Fork.ofι f w и универсальным свойством: ∀ y, g y = h y → ∃! x : X, f x = y.

LaTeX

$$$$ Nonempty(IsLimit(Fork.ofι f w)) \\iff \\forall y:\\, Y,\\; g\,y = h\,y \\to \\exists! x:\\, X,\\; f\,x = y $$$$

Lean4

@[elementwise (attr := simp)]
theorem equalizerIso_inv_comp_ι : (equalizerIso g h).inv ≫ equalizer.ι g h = Subtype.val :=
  limit.isoLimitCone_inv_π equalizerLimit WalkingParallelPair.zero

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