range_toSubgraph — Mathlib

English

The image of the mapping toSubgraph is exactly the set of subgraphs of B that are isomorphic to A.

Русский

Образ отображения toSubgraph равен множеству подграфов B, изоморфных A.

LaTeX

$$\mathrm{range}\;\mathrm{toSubgraph} = \{ B'\;:\; B.Subgraph \mid \operatorname{Nonempty}(A \cong_g B'.coe) \}$$

Lean4

@[simp]
theorem range_toSubgraph : .range (toSubgraph (A := A)) = {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} :=
  by
  ext H'
  constructor
  · rintro ⟨f, hf, rfl⟩
    simpa [toSubgraph] using ⟨f.isoToSubgraph⟩
  · rintro ⟨e⟩
    refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
    simp [toSubgraph, Subgraph.map_comp]

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