coe_inj

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ComponentCompl.coe_inj

English

Two components are equal if and only if their vertex-sets are equal.

Русский

Две компоненты равны тогда и только тогда, когда совпадают их множества вершин.

LaTeX

$$$$ C = D \;\iff\; (C \subseteq D) \wedge (D \subseteq C) $$$$

Lean4

theorem coe_inj {C D : G.ComponentCompl K} : (C : Set V) = (D : Set V) ↔ C = D :=
  SetLike.coe_set_eq

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

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

Разделы

Аффилиация

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