ncard_graphOn — Mathlib

English

The graph of a function restricted to s has the same cardinality as s: ncard(graphOn f for s) = ncard(s).

Русский

Граф функции, ограниченный до множества s, имеет ту же кардинальность, что и s: ncard(graphOn f) = ncard(s).

LaTeX

$$$$ \mathrm{ncard}(\mathrm{graphOn}(s, f)) = \mathrm{ncard}(s) $$$$

Lean4

@[simp]
theorem ncard_graphOn (s : Set α) (f : α → β) : (s.graphOn f).ncard = s.ncard := by
  rw [← ncard_image_of_injOn fst_injOn_graph, image_fst_graphOn]

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