edgeFinset_subset_sym2_of_support_subset

English

If the graph G has its support contained in a set s, then every edge of G lies entirely inside s; i.e., G.edgeFinset ⊆ s.toFinset.sym2.

Русский

Если поддержка графа G лежит внутри множества s, то все ребра графа G лежат внутри s: G.edgeFinset ⊆ s.toFinset.sym2.

LaTeX

$$G.edgeFinset \\subseteq s.toFinset.sym2$$

Lean4

theorem edgeFinset_subset_sym2_of_support_subset (h : G.support ⊆ s) : G.edgeFinset ⊆ s.toFinset.sym2 :=
  by
  simp_rw [subset_iff, Sym2.forall, mem_edgeFinset, mem_edgeSet, mk_mem_sym2_iff, Set.mem_toFinset]
  intro _ _ hadj
  exact ⟨h ⟨_, hadj⟩, h ⟨_, hadj.symm⟩⟩

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