biUnion_supp_eq_supp — Mathlib

English

Under a graph inclusion G ≤ G', the union over all components c of G of those with c.supp ⊆ c'.supp equals c'.supp.

Русский

При включении графа G в G' объединение по компонентам G отборов, удовлетворяющих условию c.supp ⊆ c'.supp, даёт ровно c'.supp.

LaTeX

$$$\\\\bigcup_{c : ConnectedComponent G} \\\\Big( \\\\{x \\\\mid c.supp \\\\subseteq c'.supp\\\\} \\\\Rightarrow x \\\\in c.supp \) = c'.supp$$$

Lean4

theorem biUnion_supp_eq_supp {G G' : SimpleGraph V} (h : G ≤ G') (c' : ConnectedComponent G') :
    ⋃ (c : ConnectedComponent G) (_ : c.supp ⊆ c'.supp), c.supp = c'.supp :=
  by
  ext v
  simp_rw [Set.mem_iUnion]
  refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩
  intro hv
  use G.connectedComponentMk v
  use c'.connectedComponentMk_supp_subset_supp h hv
  simp only [mem_supp_iff]

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