supp_injective — Mathlib

English

The map sending a connected component to its support is injective.

Русский

Отображение, отправляющее компоненту связности в её опору, инъективно.

LaTeX

$$$\\\\text{Supp}: G.ConnectedComponent \\\\to Set\ V \\\\text{ is injective}$$$

Lean4

@[ext]
theorem supp_injective : Function.Injective (ConnectedComponent.supp : G.ConnectedComponent → Set V) :=
  by
  refine ConnectedComponent.ind₂ ?_
  simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq]
  intro v w h
  rw [reachable_comm, h]

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