natCard_graphOn — Mathlib

English

Let S be a subset of α and f: α → β. The graph of f over S, namely the set of pairs (a, f(a)) with a ∈ S, has the same cardinality as S.

Русский

Пусть S ⊆ α и f: α → β. График функции на S, состоящий из пар (a, f(a)) с a ∈ S, имеет ту же кардинальность, что и S.

LaTeX

$$$\operatorname{card}(\{(a,f(a)) : a \in s\}) = \operatorname{card}(s)$$$

Lean4

theorem natCard_graphOn (s : Set α) (f : α → β) : Nat.card (s.graphOn f) = Nat.card s := by
  rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]

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