equalizer_eq_top — Mathlib

English

For algebra homomorphisms φ, ψ, the equalizer equals the top subalgebra exactly when φ = ψ.

Русский

Для алгебраических отображений φ, ψ равенство множества элементов, где φ и ψ совпадают, равняется верху тогда и только тогда, когда φ = ψ.

LaTeX

$$$ \\mathrm{equalizer\_eq\_top} : \\mathrm{equalizer}(\\varphi,\\psi) = \\top \\; \\iff\\; \\varphi = \\psi $$$

Lean4

@[simp]
theorem equalizer_eq_top {φ ψ : F} : equalizer φ ψ = ⊤ ↔ φ = ψ := by simp [SetLike.ext_iff, DFunLike.ext_iff]

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