supp_injective — Mathlib

English

Supp is injective: different components have different supports.

Русский

Функция supp инъективна: разные компоненты имеют разные поддержки.

LaTeX

$$$$ \mathrm{Supp\,inj} : \mathrm{Function.Injective}(\mathrm{ComponentCompl.supp} : G.ComponentCompl K \to \mathrm{Set} V). $$$$

Lean4

@[ext]
theorem supp_injective : Function.Injective (ComponentCompl.supp : G.ComponentCompl K → Set V) :=
  by
  refine ConnectedComponent.ind₂ ?_
  rintro ⟨v, hv⟩ ⟨w, hw⟩ h
  simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢
  exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec

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