labelledCopyCount_pos

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.labelledCopyCount_pos

English

0 < labelledCopyCount(G,H) is equivalent to H is contained in G.

Русский

0 < labelledCopyCount(G,H) эквивалентно тому, что H вложен в G.

LaTeX

$$0 < \mathrm{labelledCopyCount}(G,H) \iff H \subseteq G$$

Lean4

@[simp]
theorem labelledCopyCount_pos : 0 < G.labelledCopyCount H ↔ H ⊑ G := by
  simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]

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

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

Разделы

Аффилиация

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