equalizer — Mathlib

English

x is in the equalizer of f and g if and only if f x = g x.

Русский

x принадлежит равнителю f и g тогда и только тогда, когда f x = g x.

LaTeX

$$$ x \\in \\mathrm{equalizer}\; f\\; g \\;\\Longleftrightarrow\\; f x = g x $$$

Lean4

/-- The equalizer of two star `R`-algebra homomorphisms. -/
def equalizer : StarSubalgebra R A
    where
  toSubalgebra := AlgHom.equalizer (f : A →ₐ[R] B) g
  star_mem' {a} (ha : f a = g a) := by simpa only [← map_star] using congrArg star ha

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