eqLocus_eq_top

Mathlib.Algebra.Module.Submodule.EqLocus

URI: https://scilib.ai/kg/mathlib#LinearMap.eqLocus_eq_top

English

The equalizer is the whole space iff the two maps are equal.

Русский

Равновесие равно всей пространству тогда и только тогда, когда отображения равны.

LaTeX

$$$eqLocus(f,g)=\top \iff f=g$$$

Lean4

@[simp]
theorem eqLocus_eq_top {f g : F} : eqLocus f g = ⊤ ↔ f = g := by simp [SetLike.ext_iff, DFunLike.ext_iff]

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

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

Разделы

Аффилиация

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