equalizer_eq_iff — Mathlib

English

The equalizer of f and g equals A if and only if f equals g.

Русский

Равнитель f и g равен A тогда и только тогда, когда f = g.

LaTeX

$$$\\text{equalizer}(f,g) = A \\iff f = g$$$

Lean4

theorem equalizer_eq_iff : Subpresheaf.equalizer f g = A ↔ f = g :=
  by
  have := range_le_equalizer_iff f g (𝟙 _)
  simp only [Category.id_comp, range_ι] at this
  rw [← this]
  constructor
  · intro h
    rw [h]
  · intro h
    exact le_antisymm (equalizer_le f g) h

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