card

Mathlib.Data.Fin.Tuple.Sort

URI: https://scilib.ai/kg/mathlib#Tuple.graph.card

← MathLib Explorer

English

The cardinality of the graph of f equals n; i.e., |graph(f)| = n.

Русский

Число элементов графа функции f равно n; то есть |graph(f)| = n.

LaTeX

$$$|\\mathrm{graph}(f)| = n$$$

Lean4

@[simp]
theorem card (f : Fin n → α) : (graph f).card = n :=
  by
  rw [graph, Finset.card_image_of_injective]
  · exact Finset.card_fin _
  · intro _
      _
        -- Porting note: proof was `simp`

    rw [Prod.ext_iff]
    simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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