eqOn_adjoin_iff — Mathlib

English

For Hom φ and ψ, φ = ψ on adjoin_R s iff φ = ψ on s.

Русский

Для гомоморфизмов φ и ψ: φ = ψ на adjoin_R s тогда и только тогда, когда они равны на s.

LaTeX

$$$\\forall \\phi,\\psi:\\ A \\to_{{R}} B,\\ (\\phi=\\psi \\text{ на } \\operatorname{adjoin}_R s) \\iff (\\phi=\\psi \\text{ на } s)$$$

Lean4

/-- Two algebra morphisms are equal on `Algebra.span s`iff they are equal on s -/
theorem eqOn_adjoin_iff {φ ψ : A →ₐ[R] B} {s : Set A} : Set.EqOn φ ψ (adjoin R s) ↔ Set.EqOn φ ψ s :=
  by
  have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl
  simp only [← this, Set.le_eq_subset, SetLike.coe_subset_coe, adjoin_le_iff]

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