copyCount_bot — Mathlib

English

Induced containment in a complement corresponds to induced containment in the original graphs.

Русский

Вложение в дополнении графа соответствует индуцированному вложению в исходных графах.

LaTeX

$$G^{c} \subseteq_{\mathrm{ind}} H^{c} \\iff \\ G \subseteq_{\mathrm{ind}} H$$

Lean4

@[simp]
theorem copyCount_bot (G : SimpleGraph V) : copyCount G (⊥ : SimpleGraph V) = 1 := by
  classical
  rw [copyCount]
  convert
    card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }
  simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]
  refine
    ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
      Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩
  ext a b
  simp only [«Prop».bot_eq_false, Pi.bot_apply, iff_false]
  exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe

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