Transform connected component into subgraph

Stream: Is there code for X?

[Lessness]

Hi!
I have C: G.ConnectedComponent and want to say that it is equal to some given M: G.Subgraph, after transforming C into G.Subgraph. Is it possible using Mathlib?

(If I'm unclear, apologies. Foggy brain etc.)

[Kyle Miller]

I thought we had function somewhere for transforming a connected component into a subgraph, but it's not so bad to do directly. I haven't tested this, but I believe it's

(⊤ : G.Subgraph).induce C.supp = M

[Lessness]

What is T in this case? (Still a noob, not understanding things sometime.)

[Yaël Dillies]

It's the complete graph.

[Lessness]

Oh... so it's not letter T (t).

Thank you

[Kyle Miller]

It's pronounced "top" for "top of the lattice of subgraphs of G". There's also ⊥, pronounced "bot" for "bottom", which would be the empty subgraph of G in this context.

[Kyle Miller]

Yaël Dillies said:

It's the complete graph.

It's G as a subgraph of itself to be more accurate