![]() |
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 |
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.) |
Ref | Expression |
---|---|
df-grlic | ⊢ ≃𝑙𝑔𝑟 = (◡ GraphLocIso “ (V ∖ 1o)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgrlic 47801 | . 2 class ≃𝑙𝑔𝑟 | |
2 | cgrlim 47800 | . . . 4 class GraphLocIso | |
3 | 2 | ccnv 5699 | . . 3 class ◡ GraphLocIso |
4 | cvv 3488 | . . . 4 class V | |
5 | c1o 8515 | . . . 4 class 1o | |
6 | 4, 5 | cdif 3973 | . . 3 class (V ∖ 1o) |
7 | 3, 6 | cima 5703 | . 2 class (◡ GraphLocIso “ (V ∖ 1o)) |
8 | 1, 7 | wceq 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 |