cliqueFinset_eq_map

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map

English

For NoAccidental t, the Finset of 3-cliques obtained as graph t equals the image of t under toTriangle.

Русский

Для NoAccidental t финсет 3-клик графа t равен изображению t под toTriangle.

LaTeX

$$$ (graph\ t).cliqueFinset\ 3 = image\ toTriangle\ t$$$

Lean4

theorem cliqueFinset_eq_map [NoAccidental t] : (graph t).cliqueFinset 3 = t.map toTriangle := by
  simp [cliqueFinset_eq_image, map_eq_image]

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

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

Разделы

Аффилиация

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