From 9bfe1e0f9a092c9e74e406ffa0e0f61b84ac51d0 Mon Sep 17 00:00:00 2001 From: LessnessRandomness <56280933+LessnessRandomness@users.noreply.github.com> Date: Sat, 28 Dec 2024 03:19:58 +0000 Subject: [PATCH] doc: Update Maps.lean (#20207) Added missing apostrophe (G -> G') in the documentation of [SimpleGraph.Embedding](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Maps.html#SimpleGraph.Embedding) --- Mathlib/Combinatorics/SimpleGraph/Maps.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean index 4fc6a972b04d8..e27bbf65c3096 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean @@ -203,7 +203,7 @@ abbrev Hom := RelHom G.Adj G'.Adj /-- A graph embedding is an embedding `f` such that for vertices `v w : V`, -`G.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'. +`G'.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'. The notation `G ↪g G'` represents the type of graph embeddings. -/ abbrev Embedding :=