fst_injOn_graph

Mathlib.Data.Set.Prod

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

English

The first-coordinate projection is injective on the graph of f restricted to s.

Русский

Проекция по первой координате инъективна на графе f на s.

LaTeX

$$$(\operatorname{graphOn}(f,s)).\operatorname{InjOn} \mathrm{Prod.fst}$$$

Lean4

theorem fst_injOn_graph : (s.graphOn f).InjOn Prod.fst := by aesop (add simp InjOn)

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

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

Разделы

Аффилиация

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