Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-grlic Structured version   Visualization version   GIF version

Definition df-grlic 47805
Description: Two graphs are said to be locally isomorphic iff they are connected by at least one local isomorphism. (Contributed by AV, 27-Apr-2025.)
Assertion
Ref Expression
df-grlic 𝑙𝑔𝑟 = ( GraphLocIso “ (V ∖ 1o))

Detailed syntax breakdown of Definition df-grlic
StepHypRef Expression
1 cgrlic 47801 . 2 class 𝑙𝑔𝑟
2 cgrlim 47800 . . . 4 class GraphLocIso
32ccnv 5699 . . 3 class GraphLocIso
4 cvv 3488 . . . 4 class V
5 c1o 8515 . . . 4 class 1o
64, 5cdif 3973 . . 3 class (V ∖ 1o)
73, 6cima 5703 . 2 class ( GraphLocIso “ (V ∖ 1o))
81, 7wceq 1537 1 wff 𝑙𝑔𝑟 = ( GraphLocIso “ (V ∖ 1o))
Colors of variables: wff setvar class
This definition is referenced by:  brgrlic  47821  grlicrel  47823
  Copyright terms: Public domain W3C validator