ext

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#CoalgHom.ext

English

If two coalgebra homomorphisms agree on every input, they are equal

Русский

Если два коалгоморфизма совпадают на всех входах, то они равны

LaTeX

$$$$ \forall x, \phi_1 x = \phi_2 x \Rightarrow \phi_1 = \phi_2 $$$$

Lean4

@[ext]
theorem ext {φ₁ φ₂ : A →ₗc[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
  DFunLike.ext _ _ H

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru