lift_graph

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.lift_graph

English

For any a,b, (a,b) ∈ (PFun.lift f).graph if and only if f(a) = b.

Русский

Для любых a,b: (a,b) принадлежит графу (PFun.lift f) тогда и только тогда, когда f(a) = b.

LaTeX

$$$ (a,b) \\in (\\mathrm{PFun.lift}(f)).graph \\iff f(a) = b$$$

Lean4

theorem lift_graph {f : α → β} {a b} : (a, b) ∈ (f : α →. β).graph ↔ f a = b :=
  show (∃ _ : True, f a = b) ↔ f a = b by simp

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

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

Разделы

Аффилиация

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