toSubgraph_surjOn — Mathlib

English

The map toSubgraph is surjective onto the family of subgraphs isomorphic to A: for every B' in B.Subgraph with A ≃g B'.coe, there exists a copy f : A Copy B with toSubgraph f = B'.

Русский

Отображение toSubgraph отображает на все подграфы B, которые изоморфны A; для каждого такого B' существует копия f: A Copy B, такая что toSubgraph f = B'.

LaTeX

$$\forall B' : B.Subgraph, \operatorname{Nonempty}(A \cong_g B'.coe) \Rightarrow \exists f : A.Copy B, \mathrm{toSubgraph} f = B'.$$

Lean4

theorem toSubgraph_surjOn : Set.SurjOn (toSubgraph (A := A)) .univ {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} :=
  fun H' hH' ↦ by simpa

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