graphOn_inj

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.graphOn_inj

English

Two graphs on the same set s are equal if and only if the underlying functions are equal on s.

Русский

Графы на одном и том же множестве s равны тогда и только тогда, когда функции совпадают на s.

LaTeX

$$$s.graphOn f = s.graphOn g \iff s.EqOn f g$$$

Lean4

@[simp]
theorem graphOn_inj {g : α → β} : s.graphOn f = s.graphOn g ↔ s.EqOn f g := by simp [Set.ext_iff, forall_swap, EqOn]

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

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

Разделы

Аффилиация

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