graphOn_nonempty — Mathlib

English

Let s be a subset of α and f: α → β. Then the graph of f over s is nonempty if and only if s is nonempty.

Русский

Пусть s ⊆ α и f: α → β. Граф функции f над множеством s непуст тогда и только тогда, когда s непусто.

LaTeX

$$$ (\operatorname{graphOn}(f,s) \neq \varnothing) \iff (s \neq \varnothing) $$$

Lean4

@[simp]
theorem graphOn_nonempty : (s.graphOn f).Nonempty ↔ s.Nonempty :=
  image_nonempty

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