instFintypeOfDecidableEqOfDecidableRelAdj

English

Instance [DecidableEq V] [Fintype V] [DecidableRel G.Adj] implies Fintype G.Subgraph.

Русский

При условии DecidableEq V, Fintype V и DecidableRel G.Adj существует Fintype для G.Subgraph.

LaTeX

$$$ Fintype G.Subgraph $$$

Lean4

instance [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Fintype G.Subgraph :=
  by
  refine
    .ofBijective (α :=
      { H : Finset V × (V → V → Bool) //
        (∀ a b, H.2 a b → G.Adj a b) ∧ (∀ a b, H.2 a b → a ∈ H.1) ∧ ∀ a b, H.2 a b = H.2 b a })
      (fun H ↦ ⟨H.1.1, fun a b ↦ H.1.2 a b, @H.2.1, @H.2.2.1, by simp [Symmetric, H.2.2.2]⟩) ⟨?_, fun H ↦ ?_⟩
  · rintro ⟨⟨_, _⟩, -⟩ ⟨⟨_, _⟩, -⟩
    simp [funext_iff]
  ·
    classical
      exact
      ⟨⟨(H.verts.toFinset, fun a b ↦ H.Adj a b), fun a b ↦ by simpa using H.adj_sub, fun a b ↦ by
          simpa using H.edge_vert, by simp [H.adj_comm]⟩,
        by simp⟩

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