disjiUnion_supp_toFinset_eq_supp_toFinset

English

A disjoint union over connected components contained in a fixed component equals the fixed component's support as a finset.

Русский

Расщепление по попарно непересекающимся компонентам, попавшим в фиксированную компоненту, даёт ту же подмножество, что и supp фиксированной компоненты.

LaTeX

$$$\text{disjiUnion} \{ c : G.ConnectedComponent \mid c.supp \subseteq c'.supp \} (c.\,supp.\toFinset) = c'.supp.toFinset$$$

Lean4

theorem disjiUnion_supp_toFinset_eq_supp_toFinset {G' : SimpleGraph V} (h : G ≤ G') (c' : ConnectedComponent G')
    [Fintype c'.supp] [DecidablePred fun c : G.ConnectedComponent ↦ c.supp ⊆ c'.supp] :
    .disjiUnion {c : ConnectedComponent G | c.supp ⊆ c'.supp} (fun c ↦ c.supp.toFinset)
        (fun x _ y _ hxy ↦ by simpa using pairwise_disjoint_supp_connectedComponent _ hxy) =
      c'.supp.toFinset :=
  Finset.coe_injective <| by simpa using ConnectedComponent.biUnion_supp_eq_supp h _

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