English
Let G be a simple graph and f an embedding of its vertex set α into β. If G has edge-disjoint triangles, then the relabeled graph G.map f also has edge-disjoint triangles.
Русский
Пусть G — простой граф, а f — вложение вершин α в β. Если у G существуют непересекающиеся по рёбрам треугольники, то граф, полученный после отображения через f, G.map f, также имеет непересекающиеся по рёбрам треугольники.
LaTeX
$$$\\forall f:\\alpha\\hookrightarrow\\beta\\;\\forall G:\\text{SimpleGraph}\\,\\alpha,\\; G\\text{ EdgeDisjointTriangles} \\Rightarrow (G.map\\ f)\\text{ EdgeDisjointTriangles}$$$
Lean4
theorem map (f : α ↪ β) (hG : G.EdgeDisjointTriangles) : (G.map f).EdgeDisjointTriangles :=
by
rw [EdgeDisjointTriangles, cliqueSet_map (by simp : 3 ≠ 1), (Finset.map_injective f).injOn.pairwise_image]
classical
rintro s hs t ht hst
dsimp [Function.onFun]
rw [← coe_inter, ← map_inter, coe_map, coe_inter]
exact (hG hs ht hst).image _
