mem_graphOn — Mathlib

English

A point x belongs to the graph of f on set s iff its first projection lies in s and the second component equals f of the first.

Русский

Точка x принадлежит графику функции f на множестве s тогда и только тогда, когда первая координата x принадлежит s и вторая координата равна f от первой.

LaTeX

$$$$ x \\in s.\\mathrm{graphOn} f \\;\\Longleftrightarrow\\; x.1 \\in s \\wedge f(x.1) = x.2. $$$$

Lean4

@[simp]
theorem mem_graphOn : x ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2 := by aesop (add simp graphOn)

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